1 include "logic/equality.ma".
3 (* Inclusion of: HWC004-1.p *)
5 (* -------------------------------------------------------------------------- *)
7 (* File : HWC004-1 : TPTP v3.7.0. Released v2.5.0. *)
9 (* Domain : Hardware Creation *)
11 (* Problem : Definitions of AND, OR and NOT *)
13 (* Version : [WO+92] axioms. *)
15 (* Axiom formulation : Ground axioms. *)
19 (* Refs : [WO+92] Wos et al. (1992), Automated Reasoning: Introduction a *)
25 (* Status : Satisfiable *)
27 (* Rating : 0.33 v3.5.0, 0.25 v3.4.0, 0.20 v3.3.0, 0.33 v3.2.0, 0.17 v3.1.0, 0.00 v2.5.0 *)
29 (* Syntax : Number of clauses : 10 ( 0 non-Horn; 10 unit; 10 RR) *)
31 (* Number of atoms : 10 ( 10 equality) *)
33 (* Maximal clause size : 1 ( 1 average) *)
35 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
37 (* Number of functors : 5 ( 2 constant; 0-2 arity) *)
39 (* Number of variables : 0 ( 0 singleton) *)
41 (* Maximal term depth : 2 ( 2 average) *)
45 (* -------------------------------------------------------------------------- *)
47 (* ----Include Definitions of AND, OR and NOT *)
49 (* Inclusion of: Axioms/HWC001-0.ax *)
51 (* -------------------------------------------------------------------------- *)
53 (* File : HWC001-0 : TPTP v3.7.0. Released v1.0.0. *)
55 (* Domain : Hardware Creation *)
57 (* Axioms : Definitions of AND, OR and NOT *)
59 (* Version : [WO+92] axioms. *)
61 (* Axiom formulation : Ground axioms. *)
65 (* Refs : [WO+92] Wos et al. (1992), Automated Reasoning: Introduction a *)
73 (* Syntax : Number of clauses : 10 ( 0 non-Horn; 10 unit; 10 RR) *)
75 (* Number of atoms : 10 ( 10 equality) *)
77 (* Maximal clause size : 1 ( 1 average) *)
79 (* Number of predicates : 1 ( 0 propositional; 2-2 arity) *)
81 (* Number of functors : 5 ( 2 constant; 0-2 arity) *)
83 (* Number of variables : 0 ( 0 singleton) *)
85 (* Maximal term depth : 2 ( 2 average) *)
89 (* -------------------------------------------------------------------------- *)
91 (* -------------------------------------------------------------------------- *)
93 (* -------------------------------------------------------------------------- *)