%------------------------------------------------------------------------------
% File : MaedMax---1.4
% Problem : RNG131-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_maedmax %d %s
% Computer : n027.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 06:50:07 PM UTC 2026
% Result : Unsatisfiable 20.71s 20.95s
% Output : CNFRefutation 20.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 10
% Syntax : Number of clauses : 85 ( 85 unt; 0 nHn; 15 RR)
% Number of literals : 85 ( 84 equ; 11 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 8 con; 0-2 aty)
% Number of variables : 133 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(eq_0,axiom,
plus(X,Y) = plus(Y,X),
file('/tmp/MaedMax_912') ).
cnf(eq_1,axiom,
plus(X,plus(Y,Z)) = plus(plus(X,Y),Z),
file('/tmp/MaedMax_912') ).
cnf(eq_2,axiom,
X = plus(zero,X),
file('/tmp/MaedMax_912') ).
cnf(eq_3,axiom,
plus(X,minus(X)) = zero,
file('/tmp/MaedMax_912') ).
cnf(eq_4,axiom,
times(X,times(Y,Z)) = times(times(X,Y),Z),
file('/tmp/MaedMax_912') ).
cnf(eq_5,axiom,
times(X,Y) = times(Y,X),
file('/tmp/MaedMax_912') ).
cnf(eq_6,axiom,
times(X,X) = sq(X),
file('/tmp/MaedMax_912') ).
cnf(eq_7,axiom,
plus(times(X,Y),times(X,Z)) = times(X,plus(Y,Z)),
file('/tmp/MaedMax_912') ).
cnf(eq_8,axiom,
plus(times(X,Y),times(Z,Y)) = times(plus(X,Z),Y),
file('/tmp/MaedMax_912') ).
cnf(eq_9,negated_conjecture,
plus(sq(plus(times(a,c),times(minus(b),d))),sq(plus(times(a,d),times(b,c)))) != times(plus(sq(a),sq(b)),plus(sq(c),sq(d))),
file('/tmp/MaedMax_912') ).
cnf(eq_10,negated_conjecture,
plus(sq(plus(times(d,minus(b)),times(c,a))),sq(plus(times(d,a),times(b,c)))) != times(plus(sq(d),sq(c)),plus(sq(b),sq(a))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[eq_9,eq_5]),eq_5]),eq_5]),eq_0]),eq_0]),eq_0]),eq_5]) ).
cnf(eq_11,plain,
minus(zero) = zero,
inference(cp,[status(thm)],[eq_2,eq_3]) ).
cnf(eq_12,plain,
plus(X,plus(Y,minus(plus(X,Y)))) = zero,
inference(cp,[status(thm)],[eq_1,eq_3]) ).
cnf(eq_13,plain,
plus(plus(X,Y),x102) = plus(Y,plus(X,x102)),
inference(cp,[status(thm)],[eq_0,eq_1]) ).
cnf(eq_14,plain,
plus(zero,x102) = plus(X,plus(minus(X),x102)),
inference(cp,[status(thm)],[eq_3,eq_1]) ).
cnf(eq_15,plain,
plus(X,zero) = X,
inference(cp,[status(thm)],[eq_0,eq_2]) ).
cnf(eq_16,plain,
times(X,plus(Z,Z)) = times(plus(X,X),Z),
inference(cp,[status(thm)],[eq_7,eq_8]) ).
cnf(eq_17,plain,
times(X,times(Y,times(X,Y))) = sq(times(X,Y)),
inference(cp,[status(thm)],[eq_4,eq_6]) ).
cnf(eq_18,plain,
times(times(X,Y),x102) = times(Y,times(X,x102)),
inference(cp,[status(thm)],[eq_5,eq_4]) ).
cnf(eq_19,plain,
times(sq(X),x102) = times(X,times(X,x102)),
inference(cp,[status(thm)],[eq_6,eq_4]) ).
cnf(eq_20,plain,
times(zero,x102) = plus(times(X,x102),times(minus(X),x102)),
inference(cp,[status(thm)],[eq_3,eq_8]) ).
cnf(eq_21,plain,
times(X,plus(Y,Y)) = times(plus(X,X),Y),
eq_16 ).
cnf(eq_22,plain,
plus(X,plus(Y,Z)) = plus(Y,plus(X,Z)),
inference(rw,[status(thm)],[eq_13,eq_1]) ).
cnf(eq_23,plain,
times(X,times(X,Y)) = times(sq(X),Y),
eq_19 ).
cnf(eq_24,plain,
times(X,times(Y,Z)) = times(Y,times(X,Z)),
inference(rw,[status(thm)],[eq_18,eq_4]) ).
cnf(eq_25,plain,
X = plus(Y,plus(minus(Y),X)),
inference(rw,[status(thm)],[eq_14,eq_2]) ).
cnf(eq_26,plain,
plus(Y,plus(X,minus(plus(X,Y)))) = zero,
inference(cp,[status(thm)],[eq_0,eq_12]) ).
cnf(eq_27,plain,
X = plus(plus(minus(Y),X),Y),
inference(cp,[status(thm)],[eq_25,eq_0]) ).
cnf(eq_28,plain,
plus(x100,zero) = plus(Y,minus(plus(minus(x100),Y))),
inference(cp,[status(thm)],[eq_12,eq_25]) ).
cnf(eq_29,plain,
plus(x100,zero) = minus(minus(x100)),
inference(cp,[status(thm)],[eq_3,eq_25]) ).
cnf(eq_30,plain,
times(x100,times(times(x100,Y),Y)) = sq(times(x100,Y)),
inference(cp,[status(thm)],[eq_5,eq_17]) ).
cnf(eq_31,plain,
times(zero,x101) = times(zero,plus(x101,x101)),
inference(cp,[status(thm)],[eq_2,eq_21]) ).
cnf(eq_32,plain,
plus(times(zero,X),times(zero,X)) = times(zero,X),
inference(rw,[status(thm)],[eq_31,eq_7]) ).
cnf(eq_33,plain,
plus(X,plus(Y,minus(plus(Y,X)))) = zero,
eq_26 ).
cnf(eq_34,plain,
times(X,times(X,sq(Y))) = sq(times(X,Y)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[eq_30,eq_4]),eq_6]) ).
cnf(eq_35,plain,
X = plus(minus(Y),plus(X,Y)),
inference(rw,[status(thm)],[eq_27,eq_1]) ).
cnf(eq_36,plain,
X = minus(minus(X)),
inference(rw,[status(thm)],[eq_29,eq_15]) ).
cnf(eq_37,plain,
X = plus(Y,minus(plus(minus(X),Y))),
inference(rw,[status(thm)],[eq_28,eq_15]) ).
cnf(eq_38,plain,
plus(times(zero,X),plus(times(zero,X),minus(times(zero,X)))) = zero,
inference(cp,[status(thm)],[eq_32,eq_12]) ).
cnf(eq_39,plain,
plus(X,x102) = plus(minus(Y),plus(plus(X,Y),x102)),
inference(cp,[status(thm)],[eq_35,eq_1]) ).
cnf(eq_40,plain,
plus(x100,minus(plus(X,x100))) = minus(X),
inference(cp,[status(thm)],[eq_36,eq_37]) ).
cnf(eq_41,plain,
plus(minus(plus(Y,minus(plus(Y,X)))),zero) = X,
inference(cp,[status(thm)],[eq_33,eq_35]) ).
cnf(eq_42,plain,
plus(X,Y) = plus(minus(Z),plus(X,plus(Z,Y))),
inference(rw,[status(thm)],[eq_39,eq_1]) ).
cnf(eq_43,plain,
zero = times(zero,X),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[eq_38,eq_3]),eq_15]) ).
cnf(eq_44,plain,
plus(X,minus(plus(Y,X))) = minus(Y),
eq_40 ).
cnf(eq_45,plain,
X = minus(plus(Y,minus(plus(Y,X)))),
inference(rw,[status(thm)],[eq_41,eq_15]) ).
cnf(eq_46,plain,
plus(times(X,Y),times(minus(X),Y)) = zero,
inference(rw,[status(thm)],[eq_20,eq_43]) ).
cnf(eq_47,plain,
plus(Z,minus(plus(X,plus(Y,Z)))) = minus(plus(X,Y)),
inference(cp,[status(thm)],[eq_1,eq_44]) ).
cnf(eq_48,plain,
plus(times(x100,X),times(X,minus(x100))) = zero,
inference(cp,[status(thm)],[eq_5,eq_46]) ).
cnf(eq_49,plain,
minus(plus(times(X,Y),minus(zero))) = times(minus(X),Y),
inference(cp,[status(thm)],[eq_46,eq_45]) ).
cnf(eq_50,plain,
plus(X,minus(plus(Y,plus(Z,X)))) = minus(plus(Y,Z)),
eq_47 ).
cnf(eq_51,plain,
minus(times(X,Y)) = times(minus(X),Y),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[eq_49,eq_11]),eq_15]) ).
cnf(eq_52,plain,
plus(times(X,Y),times(Y,minus(X))) = zero,
eq_48 ).
cnf(eq_53,plain,
plus(Y,minus(X)) = minus(plus(minus(Y),X)),
inference(cp,[status(thm)],[eq_35,eq_50]) ).
cnf(eq_54,plain,
plus(minus(X),minus(plus(x101,zero))) = minus(plus(x101,X)),
inference(cp,[status(thm)],[eq_3,eq_50]) ).
cnf(eq_55,plain,
plus(minus(X),minus(Y)) = minus(plus(Y,X)),
inference(rw,[status(thm)],[eq_54,eq_15]) ).
cnf(eq_56,plain,
plus(X,minus(Y)) = minus(plus(minus(X),Y)),
eq_53 ).
cnf(eq_57,plain,
plus(minus(times(Y,minus(X))),zero) = times(X,Y),
inference(cp,[status(thm)],[eq_52,eq_35]) ).
cnf(eq_58,plain,
minus(plus(X,minus(Y))) = plus(minus(X),Y),
inference(cp,[status(thm)],[eq_56,eq_36]) ).
cnf(eq_59,plain,
plus(X,plus(x101,plus(minus(X),x102))) = plus(x101,x102),
inference(cp,[status(thm)],[eq_36,eq_42]) ).
cnf(eq_60,plain,
minus(plus(X,Y)) = plus(minus(X),minus(Y)),
inference(cp,[status(thm)],[eq_0,eq_55]) ).
cnf(eq_61,plain,
minus(minus(plus(Y,Z))) = plus(x100,minus(minus(plus(Y,plus(Z,minus(x100)))))),
inference(cp,[status(thm)],[eq_50,eq_56]) ).
cnf(eq_62,plain,
minus(times(X,Y)) = times(minus(Y),X),
inference(cp,[status(thm)],[eq_5,eq_51]) ).
cnf(eq_63,plain,
minus(times(X,Y)) = times(Y,minus(X)),
inference(cp,[status(thm)],[eq_51,eq_5]) ).
cnf(eq_64,plain,
plus(X,Y) = plus(Z,plus(X,plus(Y,minus(Z)))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[eq_61,eq_36]),eq_36]) ).
cnf(eq_65,plain,
minus(times(X,minus(Y))) = times(Y,X),
inference(rw,[status(thm)],[eq_57,eq_15]) ).
cnf(eq_66,plain,
plus(minus(X),Y) = minus(plus(X,minus(Y))),
eq_58 ).
cnf(eq_67,plain,
plus(X,Y) = plus(Z,plus(X,plus(minus(Z),Y))),
eq_59 ).
cnf(eq_68,plain,
times(X,Y) = times(minus(Y),minus(X)),
inference(rw,[status(thm)],[eq_65,eq_51]) ).
cnf(eq_69,plain,
times(minus(X),Y) = times(minus(Y),X),
inference(rw,[status(thm)],[eq_62,eq_51]) ).
cnf(eq_70,plain,
minus(times(minus(Y),minus(X))) = times(minus(X),Y),
inference(cp,[status(thm)],[eq_68,eq_51]) ).
cnf(eq_71,plain,
times(X,minus(x100)) = times(minus(X),x100),
inference(cp,[status(thm)],[eq_5,eq_69]) ).
cnf(eq_72,plain,
times(X,minus(Y)) = times(minus(X),Y),
eq_71 ).
cnf(eq_73,plain,
times(X,minus(Y)) = times(minus(Y),X),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[eq_70,eq_51]),eq_36]) ).
cnf(eq_74,negated_conjecture,
plus(sq(plus(times(minus(minus(b)),minus(d)),times(c,a))),sq(plus(times(d,a),times(b,c)))) != times(plus(sq(d),sq(c)),plus(sq(b),sq(a))),
inference(cp,[status(thm)],[eq_68,eq_10]) ).
cnf(eq_75,negated_conjecture,
plus(times(plus(times(b,c),times(a,d)),plus(times(b,c),times(a,d))),times(plus(times(c,a),times(b,minus(d))),plus(times(c,a),times(b,minus(d))))) != times(plus(times(b,b),times(a,a)),plus(times(c,c),times(d,d))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[eq_74,eq_36]),eq_5]),eq_0]),eq_0]),eq_6]),eq_6]),eq_0]),eq_6]),eq_6]),eq_6]),eq_6]),eq_0]),eq_5]) ).
cnf(eq_76,plain,
minus(times(X,Y)) = times(X,minus(Y)),
inference(rw,[status(thm)],[eq_51,eq_72]) ).
cnf(eq_77,negated_conjecture,
plus(times(plus(times(a,d),times(b,c)),plus(times(a,d),times(b,c))),times(plus(times(b,d),minus(times(a,c))),plus(times(b,d),minus(times(a,c))))) != times(plus(times(a,a),times(b,b)),plus(times(d,d),times(c,c))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[eq_75,eq_0]),eq_0]),eq_5]),eq_76]),eq_5]),eq_76]),eq_0]),eq_0]),eq_66]),eq_66]),eq_51]),eq_76]),eq_36]),eq_0]),eq_0]) ).
cnf(eq_78,negated_conjecture,
plus(times(plus(times(a,d),times(b,c)),plus(times(a,d),times(b,c))),times(plus(times(b,d),times(minus(a),c)),plus(times(b,d),times(minus(a),c)))) != times(plus(times(a,a),times(b,b)),plus(times(d,d),times(c,c))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[eq_77,eq_63]),eq_63]),eq_5]),eq_5]) ).
cnf(eq_79,negated_conjecture,
plus(times(plus(times(a,d),times(b,c)),plus(times(a,d),times(b,c))),times(plus(times(b,d),times(minus(a),c)),plus(times(b,d),times(minus(c),a)))) != times(plus(times(a,a),times(b,b)),plus(times(d,d),times(c,c))),
inference(cp,[status(thm)],[eq_69,eq_78]) ).
cnf(eq_80,negated_conjecture,
plus(times(plus(times(a,d),times(b,c)),plus(times(a,d),times(b,c))),times(plus(times(b,d),times(minus(a),c)),plus(times(b,d),times(a,minus(c))))) != times(plus(times(a,a),times(b,b)),plus(times(d,d),times(c,c))),
inference(rw,[status(thm)],[eq_79,eq_5]) ).
cnf(eq_81,negated_conjecture,
plus(times(plus(times(b,c),times(d,a)),plus(times(b,c),times(d,a))),times(plus(times(b,d),times(minus(c),a)),plus(times(b,d),times(c,minus(a))))) != times(plus(times(d,d),times(c,c)),plus(times(b,b),times(a,a))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[eq_80,eq_5]),eq_5]),eq_5]),eq_5]),eq_0]),eq_0]),eq_5]),eq_0]),eq_5]) ).
cnf(eq_82,negated_conjecture,
plus(times(plus(times(b,c),times(d,a)),plus(times(b,c),times(d,a))),times(plus(times(b,d),times(a,minus(c))),plus(times(b,d),times(c,minus(a))))) != times(plus(times(d,d),times(c,c)),plus(times(b,b),times(a,a))),
inference(cp,[status(thm)],[eq_73,eq_81]) ).
cnf(eq_83,negated_conjecture,
plus(sq(times(b,d)),plus(sq(times(b,c)),plus(sq(times(d,a)),sq(times(c,a))))) != plus(sq(times(b,d)),plus(sq(times(b,c)),plus(sq(times(d,a)),sq(times(c,a))))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[eq_82,eq_8]),eq_76]),eq_76]),eq_4]),eq_4]),eq_5]),eq_7]),eq_7]),eq_8]),eq_24]),eq_24]),eq_24]),eq_24]),eq_4]),eq_51]),eq_6]),eq_5]),eq_6]),eq_7]),eq_4]),eq_7]),eq_0]),eq_24]),eq_76]),eq_7]),eq_34]),eq_7]),eq_6]),eq_24]),eq_76]),eq_34]),eq_24]),eq_7]),eq_5]),eq_24]),eq_1]),eq_34]),eq_76]),eq_6]),eq_22]),eq_7]),eq_24]),eq_76]),eq_24]),eq_34]),eq_0]),eq_60]),eq_36]),eq_1]),eq_22]),eq_1]),eq_1]),eq_1]),eq_22]),eq_67]),eq_64]),eq_22]),eq_22]),eq_6]),eq_6]),eq_6]),eq_6]),eq_8]),eq_23]),eq_23]),eq_7]),eq_7]),eq_7]),eq_7]),eq_34]),eq_34]),eq_34]),eq_34]),eq_5]),eq_5]),eq_1]),eq_22]) ).
cnf(bot,negated_conjecture,
$false,
inference(cn,[status(thm)],[eq_83]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : RNG131-1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.13 % Command : run_maedmax %d %s
% 0.15/0.34 % Computer : n027.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Tue May 5 05:14:34 EDT 2026
% 0.15/0.34 % CPUTime :
% 20.71/20.95 % SZS status Unsatisfiable
% 20.71/20.95 % SZS output start CNFRefutation for /tmp/MaedMax_912
% See solution above
% 20.71/20.95
%------------------------------------------------------------------------------