%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GRP178-1 : TPTP v9.2.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n007.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 : Tue May 5 04:24:41 PM UTC 2026
% Result : Unsatisfiable 181.88s 104.42s
% Output : CNFRefutation 183.08s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named i_0_467)
% Comments :
%------------------------------------------------------------------------------
cnf(monotony_lub2,axiom,
multiply(least_upper_bound(X1,X2),X3) = least_upper_bound(multiply(X1,X3),multiply(X2,X3)),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-2.ax',monotony_lub2) ).
cnf(monotony_glb2,axiom,
multiply(greatest_lower_bound(X1,X2),X3) = greatest_lower_bound(multiply(X1,X3),multiply(X2,X3)),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-2.ax',monotony_glb2) ).
cnf(monotony_lub1,axiom,
multiply(X1,least_upper_bound(X2,X3)) = least_upper_bound(multiply(X1,X2),multiply(X1,X3)),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-2.ax',monotony_lub1) ).
cnf(monotony_glb1,axiom,
multiply(X1,greatest_lower_bound(X2,X3)) = greatest_lower_bound(multiply(X1,X2),multiply(X1,X3)),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-2.ax',monotony_glb1) ).
cnf(associativity,axiom,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',associativity) ).
cnf(associativity_of_lub,axiom,
least_upper_bound(X1,least_upper_bound(X2,X3)) = least_upper_bound(least_upper_bound(X1,X2),X3),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-2.ax',associativity_of_lub) ).
cnf(associativity_of_glb,axiom,
greatest_lower_bound(X1,greatest_lower_bound(X2,X3)) = greatest_lower_bound(greatest_lower_bound(X1,X2),X3),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-2.ax',associativity_of_glb) ).
cnf(prove_p09a,negated_conjecture,
greatest_lower_bound(a,multiply(b,c)) != greatest_lower_bound(a,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_p09a) ).
cnf(lub_absorbtion,axiom,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-2.ax',lub_absorbtion) ).
cnf(glb_absorbtion,axiom,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-2.ax',glb_absorbtion) ).
cnf(symmetry_of_lub,axiom,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-2.ax',symmetry_of_lub) ).
cnf(symmetry_of_glb,axiom,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-2.ax',symmetry_of_glb) ).
cnf(left_inverse,axiom,
multiply(inverse(X1),X1) = identity,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_inverse) ).
cnf(idempotence_of_lub,axiom,
least_upper_bound(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-2.ax',idempotence_of_lub) ).
cnf(idempotence_of_gld,axiom,
greatest_lower_bound(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-2.ax',idempotence_of_gld) ).
cnf(left_identity,axiom,
multiply(identity,X1) = X1,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_identity) ).
cnf(p09a_3,hypothesis,
least_upper_bound(identity,c) = c,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p09a_3) ).
cnf(p09a_2,hypothesis,
least_upper_bound(identity,b) = b,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p09a_2) ).
cnf(p09a_1,hypothesis,
least_upper_bound(identity,a) = a,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p09a_1) ).
cnf(p09a_4,hypothesis,
greatest_lower_bound(a,b) = identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p09a_4) ).
cnf(i_0_20,axiom,
multiply(least_upper_bound(X1,X2),X3) = least_upper_bound(multiply(X1,X3),multiply(X2,X3)),
monotony_lub2,
[final] ).
cnf(i_0_21,axiom,
multiply(greatest_lower_bound(X1,X2),X3) = greatest_lower_bound(multiply(X1,X3),multiply(X2,X3)),
monotony_glb2,
[final] ).
cnf(i_0_22,axiom,
multiply(X1,least_upper_bound(X2,X3)) = least_upper_bound(multiply(X1,X2),multiply(X1,X3)),
monotony_lub1,
[final] ).
cnf(i_0_23,axiom,
multiply(X1,greatest_lower_bound(X2,X3)) = greatest_lower_bound(multiply(X1,X2),multiply(X1,X3)),
monotony_glb1,
[final] ).
cnf(i_0_24,axiom,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
associativity,
[final] ).
cnf(i_0_25,axiom,
least_upper_bound(X1,least_upper_bound(X2,X3)) = least_upper_bound(least_upper_bound(X1,X2),X3),
associativity_of_lub,
[final] ).
cnf(i_0_26,axiom,
greatest_lower_bound(X1,greatest_lower_bound(X2,X3)) = greatest_lower_bound(greatest_lower_bound(X1,X2),X3),
associativity_of_glb,
[final] ).
cnf(i_0_27,negated_conjecture,
greatest_lower_bound(a,multiply(b,c)) != greatest_lower_bound(a,c),
prove_p09a,
[final] ).
cnf(i_0_28,axiom,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = X1,
lub_absorbtion,
[final] ).
cnf(i_0_29,axiom,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = X1,
glb_absorbtion,
[final] ).
cnf(i_0_30,axiom,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
symmetry_of_lub,
[final] ).
cnf(i_0_31,axiom,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
symmetry_of_glb,
[final] ).
cnf(i_0_32,axiom,
multiply(inverse(X1),X1) = identity,
left_inverse,
[final] ).
cnf(i_0_33,axiom,
least_upper_bound(X1,X1) = X1,
idempotence_of_lub,
[final] ).
cnf(i_0_34,axiom,
greatest_lower_bound(X1,X1) = X1,
idempotence_of_gld,
[final] ).
cnf(i_0_35,axiom,
multiply(identity,X1) = X1,
left_identity,
[final] ).
cnf(i_0_36,hypothesis,
least_upper_bound(identity,c) = c,
p09a_3,
[final] ).
cnf(i_0_37,hypothesis,
least_upper_bound(identity,b) = b,
p09a_2,
[final] ).
cnf(i_0_38,hypothesis,
least_upper_bound(identity,a) = a,
p09a_1,
[final] ).
cnf(i_0_39,hypothesis,
greatest_lower_bound(a,b) = identity,
p09a_4,
[final] ).
cnf(i_0_40,axiom,
X1 = X1 ).
cnf(i_0_41,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_42,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_43,axiom,
( X1 != X2
| multiply(X1,X3) = multiply(X2,X3) ) ).
cnf(i_0_44,axiom,
( X1 != X2
| multiply(X3,X1) = multiply(X3,X2) ) ).
cnf(i_0_45,axiom,
( X1 != X2
| least_upper_bound(X1,X3) = least_upper_bound(X2,X3) ) ).
cnf(i_0_46,axiom,
( X1 != X2
| least_upper_bound(X3,X1) = least_upper_bound(X3,X2) ) ).
cnf(i_0_47,axiom,
( X1 != X2
| greatest_lower_bound(X1,X3) = greatest_lower_bound(X2,X3) ) ).
cnf(i_0_48,axiom,
( X1 != X2
| greatest_lower_bound(X3,X1) = greatest_lower_bound(X3,X2) ) ).
cnf(i_0_758,plain,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = least_upper_bound(X1,greatest_lower_bound(X1,X3)),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_760,plain,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = greatest_lower_bound(least_upper_bound(X1,X3),X1),
inference(scs_inference,[],[i_0_31,i_0_467,i_0_42,i_0_41]) ).
cnf(i_0_761,plain,
greatest_lower_bound(b,a) = least_upper_bound(identity,greatest_lower_bound(identity,X1)),
inference(scs_inference,[],[i_0_31,i_0_488,i_0_42]) ).
cnf(i_0_763,plain,
least_upper_bound(identity,greatest_lower_bound(identity,X1)) = greatest_lower_bound(b,a),
inference(scs_inference,[],[i_0_31,i_0_488,i_0_42,i_0_41]) ).
cnf(i_0_764,plain,
greatest_lower_bound(b,a) = greatest_lower_bound(identity,least_upper_bound(identity,X1)),
inference(scs_inference,[],[i_0_31,i_0_547,i_0_42]) ).
cnf(i_0_766,plain,
greatest_lower_bound(identity,least_upper_bound(identity,X1)) = greatest_lower_bound(b,a),
inference(scs_inference,[],[i_0_31,i_0_547,i_0_42,i_0_41]) ).
cnf(i_0_916,plain,
greatest_lower_bound(least_upper_bound(a,X1),a) = least_upper_bound(identity,a),
inference(scs_inference,[],[i_0_31,i_0_533,i_0_42]) ).
cnf(i_0_918,plain,
least_upper_bound(identity,a) = greatest_lower_bound(least_upper_bound(a,X1),a),
inference(scs_inference,[],[i_0_31,i_0_533,i_0_42,i_0_41]) ).
cnf(i_0_919,plain,
greatest_lower_bound(least_upper_bound(b,X1),b) = least_upper_bound(identity,b),
inference(scs_inference,[],[i_0_31,i_0_542,i_0_42]) ).
cnf(i_0_921,plain,
least_upper_bound(identity,b) = greatest_lower_bound(least_upper_bound(b,X1),b),
inference(scs_inference,[],[i_0_31,i_0_542,i_0_42,i_0_41]) ).
cnf(i_0_922,plain,
greatest_lower_bound(least_upper_bound(identity,X1),identity) = multiply(inverse(X2),X2),
inference(scs_inference,[],[i_0_31,i_0_530,i_0_42]) ).
cnf(i_0_924,plain,
multiply(inverse(X1),X1) = greatest_lower_bound(least_upper_bound(identity,X2),identity),
inference(scs_inference,[],[i_0_31,i_0_530,i_0_42,i_0_41]) ).
cnf(i_0_1064,plain,
multiply(X1,least_upper_bound(X2,X3)) = least_upper_bound(multiply(X1,X3),multiply(X1,X2)),
inference(rename_variables,[],[i_0_632]) ).
cnf(i_0_1140,plain,
least_upper_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,least_upper_bound(X3,X2)),
inference(rename_variables,[],[i_0_630]) ).
cnf(i_0_1176,plain,
least_upper_bound(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,least_upper_bound(X3,X2)),
inference(rename_variables,[],[i_0_630]) ).
cnf(i_0_1380,plain,
multiply(X1,least_upper_bound(X2,X3)) = least_upper_bound(multiply(X1,X3),multiply(X1,X2)),
inference(rename_variables,[],[i_0_632]) ).
cnf(i_0_66,plain,
multiply(least_upper_bound(X1,X1),X2) = multiply(X1,X2),
inference(scs_inference,[],[i_0_63,i_0_41]) ).
cnf(i_0_67,plain,
X1 = multiply(identity,greatest_lower_bound(X1,X1)),
inference(scs_inference,[],[i_0_53,i_0_56,i_0_63,i_0_41,i_0_42]) ).
cnf(i_0_91,plain,
multiply(identity,least_upper_bound(least_upper_bound(identity,b),least_upper_bound(identity,b))) = b,
inference(scs_inference,[],[i_0_62,i_0_21,i_0_37,i_0_41,i_0_42]) ).
cnf(i_0_92,plain,
multiply(identity,least_upper_bound(X1,X1)) = X1,
inference(rename_variables,[],[i_0_62]) ).
cnf(i_0_116,plain,
multiply(identity,least_upper_bound(X1,X1)) = X1,
inference(rename_variables,[],[i_0_62]) ).
cnf(i_0_155,plain,
multiply(identity,least_upper_bound(identity,identity)) = multiply(inverse(X1),X1),
inference(scs_inference,[],[i_0_62,i_0_32,i_0_41,i_0_42]) ).
cnf(i_0_156,plain,
multiply(identity,least_upper_bound(X1,X1)) = X1,
inference(rename_variables,[],[i_0_62]) ).
cnf(i_0_173,plain,
multiply(identity,least_upper_bound(X1,X1)) = X1,
inference(rename_variables,[],[i_0_62]) ).
cnf(i_0_186,plain,
multiply(identity,least_upper_bound(X1,X1)) = X1,
inference(rename_variables,[],[i_0_62]) ).
cnf(i_0_200,plain,
multiply(identity,least_upper_bound(identity,identity)) = greatest_lower_bound(a,b),
inference(scs_inference,[],[i_0_62,i_0_39,i_0_41,i_0_42]) ).
cnf(i_0_201,plain,
multiply(identity,least_upper_bound(X1,X1)) = X1,
inference(rename_variables,[],[i_0_62]) ).
cnf(i_0_610,plain,
multiply(identity,least_upper_bound(a,a)) = least_upper_bound(a,identity),
inference(scs_inference,[],[i_0_571,i_0_606,i_0_42]) ).
cnf(i_0_611,plain,
greatest_lower_bound(a,least_upper_bound(a,X1)) = least_upper_bound(a,identity),
inference(rename_variables,[],[i_0_606]) ).
cnf(i_0_612,plain,
multiply(identity,least_upper_bound(X1,X1)) = greatest_lower_bound(X1,least_upper_bound(X1,X2)),
inference(rename_variables,[],[i_0_571]) ).
cnf(i_0_613,plain,
least_upper_bound(a,identity) = multiply(identity,least_upper_bound(a,a)),
inference(scs_inference,[],[i_0_571,i_0_606,i_0_42,i_0_41]) ).
cnf(i_0_614,plain,
least_upper_bound(greatest_lower_bound(a,X1),a) = least_upper_bound(a,identity),
inference(scs_inference,[],[i_0_30,i_0_600,i_0_42]) ).
cnf(i_0_616,plain,
least_upper_bound(a,identity) = least_upper_bound(greatest_lower_bound(a,X1),a),
inference(scs_inference,[],[i_0_30,i_0_600,i_0_42,i_0_41]) ).
cnf(i_0_621,plain,
greatest_lower_bound(b,least_upper_bound(b,X1)) = least_upper_bound(b,identity),
inference(rename_variables,[],[i_0_609]) ).
cnf(i_0_624,plain,
least_upper_bound(greatest_lower_bound(b,X1),b) = least_upper_bound(b,identity),
inference(scs_inference,[],[i_0_30,i_0_603,i_0_42]) ).
cnf(i_0_626,plain,
least_upper_bound(b,identity) = least_upper_bound(greatest_lower_bound(b,X1),b),
inference(scs_inference,[],[i_0_30,i_0_603,i_0_42,i_0_41]) ).
cnf(i_0_666,plain,
greatest_lower_bound(b,least_upper_bound(b,X1)) = least_upper_bound(b,identity),
inference(rename_variables,[],[i_0_609]) ).
cnf(i_0_672,plain,
greatest_lower_bound(b,least_upper_bound(b,X1)) = least_upper_bound(b,identity),
inference(rename_variables,[],[i_0_609]) ).
cnf(i_0_684,plain,
multiply(inverse(X1),X1) = least_upper_bound(greatest_lower_bound(identity,X2),identity),
inference(scs_inference,[],[i_0_683,i_0_532,i_0_42]) ).
cnf(i_0_685,plain,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = least_upper_bound(greatest_lower_bound(X1,X3),X1),
inference(rename_variables,[],[i_0_683]) ).
cnf(i_0_686,plain,
least_upper_bound(greatest_lower_bound(identity,X1),identity) = multiply(inverse(X2),X2),
inference(scs_inference,[],[i_0_683,i_0_532,i_0_42,i_0_41]) ).
cnf(i_0_693,plain,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = least_upper_bound(greatest_lower_bound(X1,X3),X1),
inference(rename_variables,[],[i_0_683]) ).
cnf(i_0_710,plain,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = least_upper_bound(greatest_lower_bound(X1,X3),X1),
inference(rename_variables,[],[i_0_683]) ).
cnf(i_0_719,plain,
least_upper_bound(greatest_lower_bound(X1,X2),X1) = multiply(identity,least_upper_bound(X1,X1)),
inference(scs_inference,[],[i_0_30,i_0_510,i_0_42]) ).
cnf(i_0_720,plain,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = multiply(identity,least_upper_bound(X1,X1)),
inference(rename_variables,[],[i_0_510]) ).
cnf(i_0_722,plain,
multiply(identity,least_upper_bound(X1,X1)) = least_upper_bound(greatest_lower_bound(X1,X2),X1),
inference(scs_inference,[],[i_0_30,i_0_510,i_0_42,i_0_41]) ).
cnf(i_0_767,plain,
greatest_lower_bound(least_upper_bound(identity,X1),identity) = greatest_lower_bound(b,a),
inference(scs_inference,[],[i_0_31,i_0_766,i_0_42]) ).
cnf(i_0_769,plain,
greatest_lower_bound(b,a) = greatest_lower_bound(least_upper_bound(identity,X1),identity),
inference(scs_inference,[],[i_0_31,i_0_766,i_0_42,i_0_41]) ).
cnf(i_0_773,plain,
greatest_lower_bound(b,a) = least_upper_bound(greatest_lower_bound(identity,X1),identity),
inference(scs_inference,[],[i_0_31,i_0_750,i_0_42]) ).
cnf(i_0_775,plain,
least_upper_bound(greatest_lower_bound(identity,X1),identity) = greatest_lower_bound(b,a),
inference(scs_inference,[],[i_0_31,i_0_750,i_0_42,i_0_41]) ).
cnf(i_0_826,plain,
greatest_lower_bound(least_upper_bound(a,X1),a) = least_upper_bound(a,identity),
inference(scs_inference,[],[i_0_31,i_0_606,i_0_42]) ).
cnf(i_0_828,plain,
least_upper_bound(a,identity) = greatest_lower_bound(least_upper_bound(a,X1),a),
inference(scs_inference,[],[i_0_31,i_0_606,i_0_42,i_0_41]) ).
cnf(i_0_849,plain,
greatest_lower_bound(least_upper_bound(X1,X2),X1) = least_upper_bound(greatest_lower_bound(X1,X3),X1),
inference(scs_inference,[],[i_0_31,i_0_683,i_0_42]) ).
cnf(i_0_850,plain,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = least_upper_bound(greatest_lower_bound(X1,X3),X1),
inference(rename_variables,[],[i_0_683]) ).
cnf(i_0_852,plain,
least_upper_bound(greatest_lower_bound(X1,X2),X1) = greatest_lower_bound(least_upper_bound(X1,X3),X1),
inference(scs_inference,[],[i_0_31,i_0_683,i_0_42,i_0_41]) ).
cnf(i_0_853,plain,
greatest_lower_bound(least_upper_bound(b,X1),b) = least_upper_bound(b,identity),
inference(scs_inference,[],[i_0_31,i_0_609,i_0_42]) ).
cnf(i_0_855,plain,
least_upper_bound(b,identity) = greatest_lower_bound(least_upper_bound(b,X1),b),
inference(scs_inference,[],[i_0_31,i_0_609,i_0_42,i_0_41]) ).
cnf(i_0_882,plain,
greatest_lower_bound(least_upper_bound(X1,X2),X1) = multiply(identity,least_upper_bound(X1,X1)),
inference(scs_inference,[],[i_0_31,i_0_569,i_0_42]) ).
cnf(i_0_883,plain,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = multiply(identity,least_upper_bound(X1,X1)),
inference(rename_variables,[],[i_0_569]) ).
cnf(i_0_885,plain,
multiply(identity,least_upper_bound(X1,X1)) = greatest_lower_bound(least_upper_bound(X1,X2),X1),
inference(scs_inference,[],[i_0_31,i_0_569,i_0_42,i_0_41]) ).
cnf(i_0_944,plain,
multiply(X1,X2) = multiply(least_upper_bound(X1,X1),X2),
inference(rename_variables,[],[i_0_63]) ).
cnf(i_0_1032,plain,
multiply(X1,X2) = multiply(least_upper_bound(X1,X1),X2),
inference(rename_variables,[],[i_0_63]) ).
cnf(i_0_1133,plain,
multiply(identity,least_upper_bound(X1,X1)) = least_upper_bound(X1,greatest_lower_bound(X1,X2)),
inference(rename_variables,[],[i_0_512]) ).
cnf(i_0_1241,plain,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = greatest_lower_bound(least_upper_bound(X1,X3),X1),
inference(rename_variables,[],[i_0_760]) ).
cnf(i_0_1256,plain,
least_upper_bound(greatest_lower_bound(X1,X2),X1) = greatest_lower_bound(X1,least_upper_bound(X1,X3)),
inference(rename_variables,[],[i_0_680]) ).
cnf(i_0_1261,plain,
greatest_lower_bound(least_upper_bound(X1,X2),X1) = least_upper_bound(X1,greatest_lower_bound(X1,X3)),
inference(rename_variables,[],[i_0_757]) ).
cnf(i_0_1317,plain,
multiply(X1,X2) = multiply(least_upper_bound(X1,X1),X2),
inference(rename_variables,[],[i_0_63]) ).
cnf(i_0_1556,plain,
multiply(X1,X2) = multiply(least_upper_bound(X1,X1),X2),
inference(rename_variables,[],[i_0_63]) ).
cnf(i_0_69,plain,
multiply(identity,greatest_lower_bound(X1,X1)) = X1,
inference(scs_inference,[],[i_0_67,i_0_41]) ).
cnf(i_0_70,plain,
multiply(least_upper_bound(X1,X1),X2) = multiply(identity,multiply(X1,X2)),
inference(scs_inference,[],[i_0_66,i_0_56,i_0_67,i_0_41,i_0_42]) ).
cnf(i_0_80,plain,
multiply(least_upper_bound(X1,X1),X2) = multiply(X1,X2),
inference(rename_variables,[],[i_0_66]) ).
cnf(i_0_93,plain,
b = multiply(identity,least_upper_bound(least_upper_bound(identity,b),least_upper_bound(identity,b))),
inference(scs_inference,[],[i_0_91,i_0_41]) ).
cnf(i_0_94,plain,
multiply(X1,X2) = multiply(greatest_lower_bound(X1,X1),X2),
inference(scs_inference,[],[i_0_90,i_0_53,i_0_91,i_0_41,i_0_42]) ).
cnf(i_0_105,plain,
multiply(least_upper_bound(X1,X1),X2) = multiply(X1,X2),
inference(rename_variables,[],[i_0_66]) ).
cnf(i_0_126,plain,
multiply(least_upper_bound(X1,X1),X2) = multiply(X1,X2),
inference(rename_variables,[],[i_0_66]) ).
cnf(i_0_157,plain,
multiply(inverse(X1),X1) = multiply(identity,least_upper_bound(identity,identity)),
inference(scs_inference,[],[i_0_155,i_0_41]) ).
cnf(i_0_202,plain,
greatest_lower_bound(a,b) = multiply(identity,least_upper_bound(identity,identity)),
inference(scs_inference,[],[i_0_200,i_0_41]) ).
cnf(i_0_513,plain,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = multiply(identity,greatest_lower_bound(X1,X1)),
inference(scs_inference,[],[i_0_28,i_0_67,i_0_42]) ).
cnf(i_0_514,plain,
X1 = multiply(identity,greatest_lower_bound(X1,X1)),
inference(rename_variables,[],[i_0_67]) ).
cnf(i_0_515,plain,
multiply(identity,greatest_lower_bound(X1,X1)) = least_upper_bound(X1,greatest_lower_bound(X1,X2)),
inference(scs_inference,[],[i_0_28,i_0_67,i_0_42,i_0_41]) ).
cnf(i_0_572,plain,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = multiply(identity,greatest_lower_bound(X1,X1)),
inference(scs_inference,[],[i_0_29,i_0_67,i_0_42]) ).
cnf(i_0_573,plain,
X1 = multiply(identity,greatest_lower_bound(X1,X1)),
inference(rename_variables,[],[i_0_67]) ).
cnf(i_0_574,plain,
multiply(identity,greatest_lower_bound(X1,X1)) = greatest_lower_bound(X1,least_upper_bound(X1,X2)),
inference(scs_inference,[],[i_0_29,i_0_67,i_0_42,i_0_41]) ).
cnf(i_0_617,plain,
least_upper_bound(identity,a) = least_upper_bound(greatest_lower_bound(a,X1),a),
inference(scs_inference,[],[i_0_30,i_0_616,i_0_42]) ).
cnf(i_0_619,plain,
least_upper_bound(greatest_lower_bound(a,X1),a) = least_upper_bound(identity,a),
inference(scs_inference,[],[i_0_30,i_0_616,i_0_42,i_0_41]) ).
cnf(i_0_627,plain,
least_upper_bound(identity,b) = least_upper_bound(greatest_lower_bound(b,X1),b),
inference(scs_inference,[],[i_0_30,i_0_626,i_0_42]) ).
cnf(i_0_629,plain,
least_upper_bound(greatest_lower_bound(b,X1),b) = least_upper_bound(identity,b),
inference(scs_inference,[],[i_0_30,i_0_626,i_0_42,i_0_41]) ).
cnf(i_0_755,plain,
X1 = multiply(identity,greatest_lower_bound(X1,X1)),
inference(rename_variables,[],[i_0_67]) ).
cnf(i_0_770,plain,
greatest_lower_bound(a,b) = greatest_lower_bound(least_upper_bound(identity,X1),identity),
inference(scs_inference,[],[i_0_31,i_0_769,i_0_42]) ).
cnf(i_0_772,plain,
greatest_lower_bound(least_upper_bound(identity,X1),identity) = greatest_lower_bound(a,b),
inference(scs_inference,[],[i_0_31,i_0_769,i_0_42,i_0_41]) ).
cnf(i_0_1252,plain,
greatest_lower_bound(least_upper_bound(X1,X2),X1) = least_upper_bound(greatest_lower_bound(X1,X3),X1),
inference(rename_variables,[],[i_0_849]) ).
cnf(i_0_1271,plain,
least_upper_bound(greatest_lower_bound(X1,X2),X1) = greatest_lower_bound(least_upper_bound(X1,X3),X1),
inference(rename_variables,[],[i_0_852]) ).
cnf(i_0_1292,plain,
greatest_lower_bound(least_upper_bound(X1,X2),X1) = multiply(identity,least_upper_bound(X1,X1)),
inference(rename_variables,[],[i_0_882]) ).
cnf(i_0_1350,plain,
multiply(identity,least_upper_bound(X1,X1)) = least_upper_bound(greatest_lower_bound(X1,X2),X1),
inference(rename_variables,[],[i_0_722]) ).
cnf(i_0_1450,plain,
least_upper_bound(greatest_lower_bound(X1,X2),X1) = multiply(identity,least_upper_bound(X1,X1)),
inference(rename_variables,[],[i_0_719]) ).
cnf(i_0_72,plain,
multiply(identity,multiply(X1,X2)) = multiply(least_upper_bound(X1,X1),X2),
inference(scs_inference,[],[i_0_70,i_0_41]) ).
cnf(i_0_73,plain,
multiply(identity,least_upper_bound(X1,X1)) = multiply(identity,X1),
inference(scs_inference,[],[i_0_62,i_0_56,i_0_70,i_0_41,i_0_42]) ).
cnf(i_0_97,plain,
multiply(greatest_lower_bound(X1,X1),X2) = multiply(X1,X2),
inference(scs_inference,[],[i_0_94,i_0_41]) ).
cnf(i_0_99,plain,
multiply(identity,greatest_lower_bound(X1,X1)) = X1,
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_144,plain,
multiply(identity,greatest_lower_bound(X1,X1)) = X1,
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_147,plain,
multiply(least_upper_bound(X1,X1),X2) = multiply(identity,multiply(X1,X2)),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_158,plain,
multiply(identity,greatest_lower_bound(identity,identity)) = multiply(inverse(X1),X1),
inference(scs_inference,[],[i_0_154,i_0_69,i_0_155,i_0_41,i_0_42]) ).
cnf(i_0_159,plain,
multiply(identity,greatest_lower_bound(X1,X1)) = X1,
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_176,plain,
multiply(identity,greatest_lower_bound(X1,X1)) = X1,
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_195,plain,
multiply(identity,greatest_lower_bound(X1,X1)) = X1,
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_203,plain,
multiply(identity,greatest_lower_bound(identity,identity)) = greatest_lower_bound(a,b),
inference(scs_inference,[],[i_0_199,i_0_69,i_0_200,i_0_41,i_0_42]) ).
cnf(i_0_204,plain,
multiply(identity,greatest_lower_bound(X1,X1)) = X1,
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_620,plain,
multiply(identity,greatest_lower_bound(b,b)) = least_upper_bound(b,identity),
inference(scs_inference,[],[i_0_574,i_0_609,i_0_42]) ).
cnf(i_0_622,plain,
multiply(identity,greatest_lower_bound(X1,X1)) = greatest_lower_bound(X1,least_upper_bound(X1,X2)),
inference(rename_variables,[],[i_0_574]) ).
cnf(i_0_623,plain,
least_upper_bound(b,identity) = multiply(identity,greatest_lower_bound(b,b)),
inference(scs_inference,[],[i_0_574,i_0_609,i_0_42,i_0_41]) ).
cnf(i_0_723,plain,
least_upper_bound(greatest_lower_bound(X1,X2),X1) = multiply(identity,greatest_lower_bound(X1,X1)),
inference(scs_inference,[],[i_0_30,i_0_513,i_0_42]) ).
cnf(i_0_724,plain,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = multiply(identity,greatest_lower_bound(X1,X1)),
inference(rename_variables,[],[i_0_513]) ).
cnf(i_0_726,plain,
multiply(identity,greatest_lower_bound(X1,X1)) = least_upper_bound(greatest_lower_bound(X1,X2),X1),
inference(scs_inference,[],[i_0_30,i_0_513,i_0_42,i_0_41]) ).
cnf(i_0_886,plain,
greatest_lower_bound(least_upper_bound(X1,X2),X1) = multiply(identity,greatest_lower_bound(X1,X1)),
inference(scs_inference,[],[i_0_31,i_0_572,i_0_42]) ).
cnf(i_0_887,plain,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = multiply(identity,greatest_lower_bound(X1,X1)),
inference(rename_variables,[],[i_0_572]) ).
cnf(i_0_889,plain,
multiply(identity,greatest_lower_bound(X1,X1)) = greatest_lower_bound(least_upper_bound(X1,X2),X1),
inference(scs_inference,[],[i_0_31,i_0_572,i_0_42,i_0_41]) ).
cnf(i_0_911,plain,
multiply(identity,greatest_lower_bound(X1,X1)) = least_upper_bound(X1,greatest_lower_bound(X1,X2)),
inference(rename_variables,[],[i_0_515]) ).
cnf(i_0_1022,plain,
multiply(X1,X2) = multiply(greatest_lower_bound(X1,X1),X2),
inference(rename_variables,[],[i_0_94]) ).
cnf(i_0_1090,plain,
multiply(X1,X2) = multiply(greatest_lower_bound(X1,X1),X2),
inference(rename_variables,[],[i_0_94]) ).
cnf(c_0_1079,axiom,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
i_0_24 ).
cnf(c_0_1080,axiom,
multiply(inverse(X1),X1) = identity,
i_0_32 ).
cnf(c_0_1081,axiom,
multiply(identity,X1) = X1,
i_0_35 ).
cnf(c_0_1082,axiom,
greatest_lower_bound(X1,least_upper_bound(X1,X2)) = X1,
i_0_29 ).
cnf(c_0_1083,hypothesis,
least_upper_bound(identity,c) = c,
i_0_36 ).
cnf(c_0_1084,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1079,c_0_1080]),c_0_1081]) ).
cnf(c_0_1085,axiom,
least_upper_bound(X1,greatest_lower_bound(X1,X2)) = X1,
i_0_28 ).
cnf(c_0_1086,axiom,
greatest_lower_bound(X1,X2) = greatest_lower_bound(X2,X1),
i_0_31 ).
cnf(c_0_1087,axiom,
greatest_lower_bound(X1,greatest_lower_bound(X2,X3)) = greatest_lower_bound(greatest_lower_bound(X1,X2),X3),
i_0_26 ).
cnf(c_0_1088,hypothesis,
greatest_lower_bound(identity,c) = identity,
inference(spm,[status(thm)],[c_0_1082,c_0_1083]) ).
cnf(c_0_1089,plain,
multiply(X1,least_upper_bound(X2,X3)) = least_upper_bound(multiply(X1,X3),multiply(X1,X2)),
i_0_1064 ).
cnf(c_0_1090,plain,
multiply(inverse(inverse(X1)),identity) = X1,
inference(spm,[status(thm)],[c_0_1084,c_0_1080]) ).
cnf(c_0_1091,plain,
multiply(inverse(inverse(X1)),X2) = multiply(X1,X2),
inference(spm,[status(thm)],[c_0_1084,c_0_1084]) ).
cnf(c_0_1092,axiom,
multiply(greatest_lower_bound(X1,X2),X3) = greatest_lower_bound(multiply(X1,X3),multiply(X2,X3)),
i_0_21 ).
cnf(c_0_1093,plain,
least_upper_bound(X1,greatest_lower_bound(X2,X1)) = X1,
inference(spm,[status(thm)],[c_0_1085,c_0_1086]) ).
cnf(c_0_1094,hypothesis,
greatest_lower_bound(identity,greatest_lower_bound(c,X1)) = greatest_lower_bound(identity,X1),
inference(spm,[status(thm)],[c_0_1087,c_0_1088]) ).
cnf(c_0_1095,axiom,
least_upper_bound(X1,X2) = least_upper_bound(X2,X1),
i_0_30 ).
cnf(c_0_1096,plain,
multiply(inverse(X1),least_upper_bound(X2,X1)) = least_upper_bound(identity,multiply(inverse(X1),X2)),
inference(spm,[status(thm)],[c_0_1089,c_0_1080]) ).
cnf(c_0_1097,hypothesis,
least_upper_bound(identity,b) = b,
i_0_37 ).
cnf(c_0_1098,plain,
multiply(X1,identity) = X1,
inference(rw,[status(thm)],[c_0_1090,c_0_1091]) ).
cnf(c_0_1099,plain,
greatest_lower_bound(X1,multiply(X2,X1)) = multiply(greatest_lower_bound(identity,X2),X1),
inference(spm,[status(thm)],[c_0_1092,c_0_1081]) ).
cnf(c_0_1100,plain,
least_upper_bound(X1,greatest_lower_bound(X2,greatest_lower_bound(X3,X1))) = X1,
inference(spm,[status(thm)],[c_0_1093,c_0_1087]) ).
cnf(c_0_1101,hypothesis,
greatest_lower_bound(identity,greatest_lower_bound(X1,c)) = greatest_lower_bound(identity,X1),
inference(spm,[status(thm)],[c_0_1094,c_0_1086]) ).
cnf(c_0_1102,plain,
greatest_lower_bound(X1,least_upper_bound(X2,X1)) = X1,
inference(spm,[status(thm)],[c_0_1082,c_0_1095]) ).
cnf(c_0_1103,hypothesis,
least_upper_bound(identity,inverse(b)) = identity,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1096,c_0_1097]),c_0_1080]),c_0_1098]) ).
cnf(c_0_1104,hypothesis,
greatest_lower_bound(X1,multiply(c,X1)) = X1,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1099,c_0_1088]),c_0_1081]) ).
cnf(c_0_1105,hypothesis,
greatest_lower_bound(a,b) = identity,
i_0_39 ).
cnf(c_0_1106,hypothesis,
least_upper_bound(c,greatest_lower_bound(identity,X1)) = c,
inference(spm,[status(thm)],[c_0_1100,c_0_1101]) ).
cnf(c_0_1107,hypothesis,
greatest_lower_bound(identity,inverse(b)) = inverse(b),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1102,c_0_1103]),c_0_1086]) ).
cnf(c_0_1108,plain,
least_upper_bound(X1,multiply(X1,X2)) = multiply(X1,least_upper_bound(identity,X2)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1089,c_0_1098]),c_0_1095]) ).
cnf(c_0_1109,hypothesis,
least_upper_bound(X1,multiply(c,X1)) = multiply(c,X1),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1093,c_0_1104]),c_0_1095]) ).
cnf(c_0_1110,hypothesis,
greatest_lower_bound(b,a) = identity,
inference(rw,[status(thm)],[c_0_1105,c_0_1086]) ).
cnf(c_0_1111,hypothesis,
least_upper_bound(c,inverse(b)) = c,
inference(spm,[status(thm)],[c_0_1106,c_0_1107]) ).
cnf(c_0_1112,plain,
inverse(inverse(X1)) = X1,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1091,c_0_1098]),c_0_1098]) ).
cnf(c_0_1113,hypothesis,
least_upper_bound(X1,multiply(X1,c)) = multiply(X1,c),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1108,c_0_1109]),c_0_1098]),c_0_1098]) ).
cnf(c_0_1114,hypothesis,
greatest_lower_bound(b,greatest_lower_bound(a,X1)) = greatest_lower_bound(identity,X1),
inference(spm,[status(thm)],[c_0_1087,c_0_1110]) ).
cnf(c_0_1115,plain,
least_upper_bound(identity,multiply(b,c)) = multiply(b,c),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1096,c_0_1111]),c_0_1112]),c_0_1112]) ).
cnf(c_0_1116,plain,
greatest_lower_bound(X1,greatest_lower_bound(least_upper_bound(X2,X1),X3)) = greatest_lower_bound(X1,X3),
inference(spm,[status(thm)],[c_0_1087,c_0_1102]) ).
cnf(c_0_1117,hypothesis,
greatest_lower_bound(X1,multiply(X1,c)) = X1,
inference(spm,[status(thm)],[c_0_1082,c_0_1113]) ).
cnf(c_0_1118,hypothesis,
least_upper_bound(greatest_lower_bound(identity,X1),greatest_lower_bound(a,X1)) = greatest_lower_bound(a,X1),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1093,c_0_1114]),c_0_1095]) ).
cnf(c_0_1119,plain,
greatest_lower_bound(identity,multiply(b,c)) = identity,
inference(spm,[status(thm)],[c_0_1082,c_0_1115]) ).
cnf(c_0_1120,hypothesis,
greatest_lower_bound(X1,multiply(least_upper_bound(X2,X1),c)) = X1,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1116,c_0_1117]),c_0_1102]) ).
cnf(c_0_1121,hypothesis,
least_upper_bound(identity,greatest_lower_bound(a,multiply(b,c))) = greatest_lower_bound(a,multiply(b,c)),
inference(spm,[status(thm)],[c_0_1118,c_0_1119]) ).
cnf(c_0_1122,negated_conjecture,
greatest_lower_bound(a,multiply(b,c)) != greatest_lower_bound(a,c),
i_0_27 ).
cnf(c_0_1123,hypothesis,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1120,c_0_1121]),c_0_1087]),c_0_1092]),c_0_1114]),c_0_1119]),c_0_1081]),c_0_1122]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRP178-1 : TPTP v9.2.1. Bugfixed v1.2.1.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n007.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Mon May 4 18:26:39 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.35 % start to proof: theBenchmark
% 181.88/104.42 % Version : CSE_E---1.7
% 181.88/104.42 % Problem : theBenchmark.p
% 181.88/104.42 % SZS status Unsatisfiable for theBenchmark.p
% 181.88/104.42 % SZS output start CNFRefutation
% See solution above
% 183.08/105.67 % Total time : 103.384s
%------------------------------------------------------------------------------