%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LAT088-1 : TPTP v8.1.2. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:29:14 EDT 2024
% Result : Unsatisfiable 120.56s 120.80s
% Output : Refutation 120.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 9
% Syntax : Number of clauses : 43 ( 28 unt; 0 nHn; 12 RR)
% Number of literals : 61 ( 60 equ; 19 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 3 ( 3 usr; 1 con; 0-2 aty)
% Number of variables : 125 ( 36 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_normal_axioms_1,negated_conjecture,
meet(a,a) != a,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_normal_axioms_1) ).
cnf(symmetry,axiom,
( X3 != X4
| X4 = X3 ),
theory(equality) ).
cnf(transitivity,axiom,
( X6 != X7
| X7 != X8
| X6 = X8 ),
theory(equality) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c1,axiom,
( X50 != X51
| X52 != X53
| meet(X50,X52) = meet(X51,X53) ),
theory(equality) ).
cnf(wal_absorbtion_4,axiom,
meet(meet(join(X19,X20),join(X18,X19)),X19) = X19,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wal_absorbtion_4) ).
cnf(c12,plain,
( X99 != meet(meet(join(X97,X98),join(X96,X97)),X97)
| X99 = X97 ),
inference(resolution,[status(thm)],[wal_absorbtion_4,transitivity]) ).
cnf(c65,plain,
( X58 != X57
| meet(X58,X59) = meet(X57,X59) ),
inference(resolution,[status(thm)],[c1,reflexivity]) ).
cnf(wal_absorbtion_5,axiom,
join(join(meet(X22,X23),meet(X21,X22)),X22) = X22,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wal_absorbtion_5) ).
cnf(c14,plain,
( X107 != join(join(meet(X105,X106),meet(X104,X105)),X105)
| X107 = X105 ),
inference(resolution,[status(thm)],[wal_absorbtion_5,transitivity]) ).
cnf(c0,axiom,
( X36 != X37
| X38 != X39
| join(X36,X38) = join(X37,X39) ),
theory(equality) ).
cnf(c31,plain,
( X44 != X45
| join(X44,X43) = join(X45,X43) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(c26,plain,
( X152 != X153
| join(X152,meet(meet(join(X150,X149),join(X151,X150)),X150)) = join(X153,X150) ),
inference(resolution,[status(thm)],[c0,wal_absorbtion_4]) ).
cnf(c229,plain,
join(X239,meet(meet(join(X241,X242),join(X240,X241)),X241)) = join(X239,X241),
inference(resolution,[status(thm)],[c26,reflexivity]) ).
cnf(c646,plain,
join(X339,X336) = join(X339,meet(meet(join(X336,X338),join(X337,X336)),X336)),
inference(resolution,[status(thm)],[c229,symmetry]) ).
cnf(c922,plain,
join(join(X2522,X2525),X2524) = join(join(X2522,meet(meet(join(X2525,X2523),join(X2521,X2525)),X2525)),X2524),
inference(resolution,[status(thm)],[c646,c31]) ).
cnf(c22582,plain,
join(join(meet(X2527,X2526),X2527),X2527) = X2527,
inference(resolution,[status(thm)],[c922,c14]) ).
cnf(c22639,plain,
( X2692 != X2690
| meet(X2692,join(join(meet(X2693,X2691),X2693),X2693)) = meet(X2690,X2693) ),
inference(resolution,[status(thm)],[c22582,c1]) ).
cnf(c24720,plain,
meet(X2696,join(join(meet(X2695,X2694),X2695),X2695)) = meet(X2696,X2695),
inference(resolution,[status(thm)],[c22639,reflexivity]) ).
cnf(c25002,plain,
meet(X2704,X2702) = meet(X2704,join(join(meet(X2702,X2703),X2702),X2702)),
inference(resolution,[status(thm)],[c24720,symmetry]) ).
cnf(c25125,plain,
meet(meet(X3207,X3206),X3205) = meet(meet(X3207,join(join(meet(X3206,X3204),X3206),X3206)),X3205),
inference(resolution,[status(thm)],[c25002,c65]) ).
cnf(c34324,plain,
meet(meet(join(X3209,X3208),X3209),X3209) = X3209,
inference(resolution,[status(thm)],[c25125,c12]) ).
cnf(c34427,plain,
( X3459 != X3458
| meet(X3459,meet(meet(join(X3460,X3461),X3460),X3460)) = meet(X3458,X3460) ),
inference(resolution,[status(thm)],[c34324,c1]) ).
cnf(c38984,plain,
meet(X3469,meet(meet(join(X3468,X3470),X3468),X3468)) = meet(X3469,X3468),
inference(resolution,[status(thm)],[c34427,reflexivity]) ).
cnf(c39276,plain,
( X3700 != meet(X3697,meet(meet(join(X3699,X3698),X3699),X3699))
| X3700 = meet(X3697,X3699) ),
inference(resolution,[status(thm)],[c38984,transitivity]) ).
cnf(c34429,plain,
( X3220 != meet(meet(join(X3218,X3219),X3218),X3218)
| X3220 = X3218 ),
inference(resolution,[status(thm)],[c34324,transitivity]) ).
cnf(wal_absorbtion_1,axiom,
join(meet(X9,X10),meet(X9,join(X9,X10))) = X9,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wal_absorbtion_1) ).
cnf(c5,plain,
X25 = join(meet(X25,X24),meet(X25,join(X25,X24))),
inference(resolution,[status(thm)],[wal_absorbtion_1,symmetry]) ).
cnf(c86,plain,
meet(X204,X203) = meet(join(meet(X204,X205),meet(X204,join(X204,X205))),X203),
inference(resolution,[status(thm)],[c65,c5]) ).
cnf(c478,plain,
meet(meet(X2280,X2278),X2279) = meet(meet(join(meet(X2280,X2281),meet(X2280,join(X2280,X2281))),X2278),X2279),
inference(resolution,[status(thm)],[c86,c65]) ).
cnf(c18624,plain,
meet(meet(X2282,join(X2283,meet(X2282,X2284))),meet(X2282,X2284)) = meet(X2282,X2284),
inference(resolution,[status(thm)],[c478,c12]) ).
cnf(c18700,plain,
( X2298 != meet(meet(X2297,join(X2296,meet(X2297,X2299))),meet(X2297,X2299))
| X2298 = meet(X2297,X2299) ),
inference(resolution,[status(thm)],[c18624,transitivity]) ).
cnf(c34367,plain,
meet(meet(X3237,meet(X3237,X3236)),meet(X3237,X3236)) = meet(X3237,X3236),
inference(resolution,[status(thm)],[c25125,c18700]) ).
cnf(c35367,plain,
( X3589 != meet(meet(X3587,meet(X3587,X3588)),meet(X3587,X3588))
| X3589 = meet(X3587,X3588) ),
inference(resolution,[status(thm)],[c34367,transitivity]) ).
cnf(c39292,plain,
meet(meet(join(X3478,X3479),X3478),meet(meet(join(X3478,X3477),X3478),X3478)) = X3478,
inference(resolution,[status(thm)],[c38984,c34429]) ).
cnf(c39510,plain,
X3482 = meet(meet(join(X3482,X3480),X3482),meet(meet(join(X3482,X3481),X3482),X3482)),
inference(resolution,[status(thm)],[c39292,symmetry]) ).
cnf(c39582,plain,
meet(X9496,X9493) = meet(meet(meet(join(X9496,X9494),X9496),meet(meet(join(X9496,X9495),X9496),X9496)),X9493),
inference(resolution,[status(thm)],[c39510,c65]) ).
cnf(c171204,plain,
meet(X9497,meet(meet(join(X9497,X9498),X9497),X9497)) = meet(meet(join(X9497,X9498),X9497),X9497),
inference(resolution,[status(thm)],[c39582,c35367]) ).
cnf(c171323,plain,
meet(X9499,meet(meet(join(X9499,X9500),X9499),X9499)) = X9499,
inference(resolution,[status(thm)],[c171204,c34429]) ).
cnf(c171550,plain,
X9502 = meet(X9502,meet(meet(join(X9502,X9501),X9502),X9502)),
inference(resolution,[status(thm)],[c171323,symmetry]) ).
cnf(c171714,plain,
X9507 = meet(X9507,X9507),
inference(resolution,[status(thm)],[c171550,c39276]) ).
cnf(c172085,plain,
meet(X9508,X9508) = X9508,
inference(resolution,[status(thm)],[c171714,symmetry]) ).
cnf(c172155,plain,
$false,
inference(resolution,[status(thm)],[c172085,prove_normal_axioms_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : LAT088-1 : TPTP v8.1.2. Released v2.6.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n020.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 12:59:38 EDT 2024
% 0.14/0.35 % CPUTime :
% 120.56/120.80 % Version: 1.5
% 120.56/120.80 % SZS status Unsatisfiable
% 120.56/120.80 % SZS output start CNFRefutation
% See solution above
% 120.56/120.80
% 120.56/120.80 % Initial clauses : 11
% 120.56/120.80 % Processed clauses : 1343
% 120.56/120.80 % Factors computed : 3
% 120.56/120.80 % Resolvents computed: 172357
% 120.56/120.80 % Tautologies deleted: 2
% 120.56/120.80 % Forward subsumed : 1609
% 120.56/120.80 % Backward subsumed : 22
% 120.56/120.80 % -------- CPU Time ---------
% 120.56/120.80 % User time : 119.997 s
% 120.56/120.80 % System time : 0.449 s
% 120.56/120.80 % Total time : 120.446 s
%------------------------------------------------------------------------------