%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : REL003+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:54:39 AM UTC 2026
% Result : Theorem 265.35s 265.65s
% Output : Proof 267.73s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(maddux1_join_commutativity,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('REL001+0.ax',maddux1_join_commutativity) ).
fof(maddux2_join_associativity,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('REL001+0.ax',maddux2_join_associativity) ).
fof(maddux3_a_kind_of_de_Morgan,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('REL001+0.ax',maddux3_a_kind_of_de_Morgan) ).
fof(maddux4_definiton_of_meet,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('REL001+0.ax',maddux4_definiton_of_meet) ).
fof(composition_associativity,axiom,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('REL001+0.ax',composition_associativity) ).
fof(composition_identity,axiom,
! [X0] : composition(X0,one) = X0,
file('REL001+0.ax',composition_identity) ).
fof(composition_distributivity,axiom,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('REL001+0.ax',composition_distributivity) ).
fof(converse_idempotence,axiom,
! [X0] : converse(converse(X0)) = X0,
file('REL001+0.ax',converse_idempotence) ).
fof(converse_additivity,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('REL001+0.ax',converse_additivity) ).
fof(converse_multiplicativity,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('REL001+0.ax',converse_multiplicativity) ).
fof(converse_cancellativity,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('REL001+0.ax',converse_cancellativity) ).
fof(def_top,axiom,
! [X0] : top = join(X0,complement(X0)),
file('REL001+0.ax',def_top) ).
fof(def_zero,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('REL001+0.ax',def_zero) ).
fof(goals,conjecture,
! [X0,X1] :
( ( join(converse(X0),converse(X1)) = converse(X1)
=> join(X0,X1) = X1 )
& ( join(X0,X1) = X1
=> join(converse(X0),converse(X1)) = converse(X1) ) ),
file('theBenchmark.p',goals) ).
fof(f_1_1,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(fof_nnf,[status(thm)],[maddux1_join_commutativity]) ).
fof(f_1_2,plain,
! [U_1,U_0] : join(U_1,U_0) = join(U_0,U_1),
inference(variable_rename,[status(thm)],[f_1_1]) ).
cnf(f_1_3,plain,
join(U_1,U_0) = join(U_0,U_1),
inference(clausify,[status(thm)],[f_1_2]) ).
fof(f_2_1,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(fof_nnf,[status(thm)],[maddux2_join_associativity]) ).
fof(f_2_2,plain,
! [U_4,U_3,U_2] : join(U_4,join(U_3,U_2)) = join(join(U_4,U_3),U_2),
inference(variable_rename,[status(thm)],[f_2_1]) ).
cnf(f_2_3,plain,
join(U_4,join(U_3,U_2)) = join(join(U_4,U_3),U_2),
inference(clausify,[status(thm)],[f_2_2]) ).
fof(f_3_1,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(fof_nnf,[status(thm)],[maddux3_a_kind_of_de_Morgan]) ).
fof(f_3_2,plain,
! [U_6,U_5] : U_6 = join(complement(join(complement(U_6),complement(U_5))),complement(join(complement(U_6),U_5))),
inference(variable_rename,[status(thm)],[f_3_1]) ).
cnf(f_3_3,plain,
U_6 = join(complement(join(complement(U_6),complement(U_5))),complement(join(complement(U_6),U_5))),
inference(clausify,[status(thm)],[f_3_2]) ).
fof(f_4_1,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(fof_nnf,[status(thm)],[maddux4_definiton_of_meet]) ).
fof(f_4_2,plain,
! [U_8,U_7] : meet(U_8,U_7) = complement(join(complement(U_8),complement(U_7))),
inference(variable_rename,[status(thm)],[f_4_1]) ).
cnf(f_4_3,plain,
meet(U_8,U_7) = complement(join(complement(U_8),complement(U_7))),
inference(clausify,[status(thm)],[f_4_2]) ).
fof(f_5_1,plain,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(fof_nnf,[status(thm)],[composition_associativity]) ).
fof(f_5_2,plain,
! [U_11,U_10,U_9] : composition(U_11,composition(U_10,U_9)) = composition(composition(U_11,U_10),U_9),
inference(variable_rename,[status(thm)],[f_5_1]) ).
cnf(f_5_3,plain,
composition(U_11,composition(U_10,U_9)) = composition(composition(U_11,U_10),U_9),
inference(clausify,[status(thm)],[f_5_2]) ).
fof(f_6_1,plain,
! [X0] : composition(X0,one) = X0,
inference(fof_nnf,[status(thm)],[composition_identity]) ).
fof(f_6_2,plain,
! [U_12] : composition(U_12,one) = U_12,
inference(variable_rename,[status(thm)],[f_6_1]) ).
cnf(f_6_3,plain,
composition(U_12,one) = U_12,
inference(clausify,[status(thm)],[f_6_2]) ).
fof(f_7_1,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(fof_nnf,[status(thm)],[composition_distributivity]) ).
fof(f_7_2,plain,
! [U_15,U_14,U_13] : composition(join(U_15,U_14),U_13) = join(composition(U_15,U_13),composition(U_14,U_13)),
inference(variable_rename,[status(thm)],[f_7_1]) ).
cnf(f_7_3,plain,
composition(join(U_15,U_14),U_13) = join(composition(U_15,U_13),composition(U_14,U_13)),
inference(clausify,[status(thm)],[f_7_2]) ).
fof(f_8_1,plain,
! [X0] : converse(converse(X0)) = X0,
inference(fof_nnf,[status(thm)],[converse_idempotence]) ).
fof(f_8_2,plain,
! [U_16] : converse(converse(U_16)) = U_16,
inference(variable_rename,[status(thm)],[f_8_1]) ).
cnf(f_8_3,plain,
converse(converse(U_16)) = U_16,
inference(clausify,[status(thm)],[f_8_2]) ).
fof(f_9_1,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(fof_nnf,[status(thm)],[converse_additivity]) ).
fof(f_9_2,plain,
! [U_18,U_17] : converse(join(U_18,U_17)) = join(converse(U_18),converse(U_17)),
inference(variable_rename,[status(thm)],[f_9_1]) ).
cnf(f_9_3,plain,
converse(join(U_18,U_17)) = join(converse(U_18),converse(U_17)),
inference(clausify,[status(thm)],[f_9_2]) ).
fof(f_10_1,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(fof_nnf,[status(thm)],[converse_multiplicativity]) ).
fof(f_10_2,plain,
! [U_20,U_19] : converse(composition(U_20,U_19)) = composition(converse(U_19),converse(U_20)),
inference(variable_rename,[status(thm)],[f_10_1]) ).
cnf(f_10_3,plain,
converse(composition(U_20,U_19)) = composition(converse(U_19),converse(U_20)),
inference(clausify,[status(thm)],[f_10_2]) ).
fof(f_11_1,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(fof_nnf,[status(thm)],[converse_cancellativity]) ).
fof(f_11_2,plain,
! [U_22,U_21] : join(composition(converse(U_22),complement(composition(U_22,U_21))),complement(U_21)) = complement(U_21),
inference(variable_rename,[status(thm)],[f_11_1]) ).
cnf(f_11_3,plain,
join(composition(converse(U_22),complement(composition(U_22,U_21))),complement(U_21)) = complement(U_21),
inference(clausify,[status(thm)],[f_11_2]) ).
fof(f_12_1,plain,
! [X0] : top = join(X0,complement(X0)),
inference(fof_nnf,[status(thm)],[def_top]) ).
fof(f_12_2,plain,
! [U_23] : top = join(U_23,complement(U_23)),
inference(variable_rename,[status(thm)],[f_12_1]) ).
cnf(f_12_3,plain,
top = join(U_23,complement(U_23)),
inference(clausify,[status(thm)],[f_12_2]) ).
fof(f_13_1,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(fof_nnf,[status(thm)],[def_zero]) ).
fof(f_13_2,plain,
! [U_24] : zero = meet(U_24,complement(U_24)),
inference(variable_rename,[status(thm)],[f_13_1]) ).
cnf(f_13_3,plain,
zero = meet(U_24,complement(U_24)),
inference(clausify,[status(thm)],[f_13_2]) ).
fof(f_14_1,negated_conjecture,
~ ! [X0,X1] :
( ( join(converse(X0),converse(X1)) = converse(X1)
=> join(X0,X1) = X1 )
& ( join(X0,X1) = X1
=> join(converse(X0),converse(X1)) = converse(X1) ) ),
inference(negate,[status(cth)],[goals]) ).
fof(f_14_2,negated_conjecture,
? [X0,X1] :
( ( join(X0,X1) != X1
& join(converse(X0),converse(X1)) = converse(X1) )
| ( join(converse(X0),converse(X1)) != converse(X1)
& join(X0,X1) = X1 ) ),
inference(fof_nnf,[status(thm)],[f_14_1]) ).
fof(f_14_3,negated_conjecture,
? [U_26,U_25] :
( ( join(U_26,U_25) != U_25
& join(converse(U_26),converse(U_25)) = converse(U_25) )
| ( join(converse(U_26),converse(U_25)) != converse(U_25)
& join(U_26,U_25) = U_25 ) ),
inference(variable_rename,[status(thm)],[f_14_2]) ).
fof(f_14_4,negated_conjecture,
( ? [U_30,U_28] :
( join(U_30,U_28) != U_28
& join(converse(U_30),converse(U_28)) = converse(U_28) )
| ? [U_29,U_27] :
( join(converse(U_29),converse(U_27)) != converse(U_27)
& join(U_29,U_27) = U_27 ) ),
inference(miniscope,[status(thm)],[f_14_3]) ).
fof(f_14_5,negated_conjecture,
( ? [U_30,U_28] :
( join(U_30,U_28) != U_28
& join(converse(U_30),converse(U_28)) = converse(U_28) )
| ? [U_27] :
( join(converse(sK1),converse(U_27)) != converse(U_27)
& join(sK1,U_27) = U_27 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_29,sK1)],[f_14_4]) ).
fof(f_14_6,negated_conjecture,
( ? [U_30,U_28] :
( join(U_30,U_28) != U_28
& join(converse(U_30),converse(U_28)) = converse(U_28) )
| ( join(converse(sK1),converse(sK2)) != converse(sK2)
& join(sK1,sK2) = sK2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_27,sK2)],[f_14_5]) ).
fof(f_14_7,negated_conjecture,
( ? [U_28] :
( join(sK3,U_28) != U_28
& join(converse(sK3),converse(U_28)) = converse(U_28) )
| ( join(converse(sK1),converse(sK2)) != converse(sK2)
& join(sK1,sK2) = sK2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_30,sK3)],[f_14_6]) ).
fof(f_14_8,negated_conjecture,
( ( join(sK3,sK4) != sK4
& join(converse(sK3),converse(sK4)) = converse(sK4) )
| ( join(converse(sK1),converse(sK2)) != converse(sK2)
& join(sK1,sK2) = sK2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_28,sK4)],[f_14_7]) ).
cnf(f_14_9,negated_conjecture,
( join(converse(sK3),converse(sK4)) = converse(sK4)
| join(sK1,sK2) = sK2 ),
inference(clausify,[status(thm)],[f_14_8]) ).
cnf(f_14_10,negated_conjecture,
( join(sK3,sK4) != sK4
| join(sK1,sK2) = sK2 ),
inference(clausify,[status(thm)],[f_14_8]) ).
cnf(f_14_11,negated_conjecture,
( join(converse(sK3),converse(sK4)) = converse(sK4)
| join(converse(sK1),converse(sK2)) != converse(sK2) ),
inference(clausify,[status(thm)],[f_14_8]) ).
cnf(f_14_12,negated_conjecture,
( join(sK3,sK4) != sK4
| join(converse(sK1),converse(sK2)) != converse(sK2) ),
inference(clausify,[status(thm)],[f_14_8]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( join(Eq_x_0,Eq_x_1) = join(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( complement(Eq_x_0) = complement(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( meet(Eq_x_0,Eq_x_1) = meet(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( composition(Eq_x_0,Eq_x_1) = composition(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( converse(Eq_x_0) = converse(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL003+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 This is a FOF_THM_RFO_PEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n004.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 19 20:07:50 UTC 2026
% 0.12/0.36 % CPUTime :
% 265.35/265.65 % SZS status Theorem for theBenchmark
% 265.35/265.65 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------