%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : LCL430-2 : TPTP v9.2.1. Released v3.2.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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 7 07:27:50 PM UTC 2026
% Result : Unsatisfiable 0.59s 0.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : LCL430-2 : TPTP v9.2.1. Released v3.2.0.
% 0.00/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n002.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Thu May 7 12:33:02 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.59/0.61 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.59/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.59/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.59/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.59/0.61 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.59/0.61 Execution resolution_1 ended with status: unsatisfiable
% 0.59/0.61 Used heuristic: resolution_1
% 0.59/0.61
% 0.59/0.61 Input Clauses:
% 0.59/0.61
% 0.59/0.61 Predicates: c_in c_lessequals
% 0.59/0.61 Fol Constants: c_PropLog_Opl_Ofalse c_emptyset v_p t_a v_F v_t v_v
% 0.59/0.61 Fol Functions: tc_PropLog_Opl tc_set c_minus c_PropLog_Othms c_insert c_PropLog_Ohyps c_PropLog_Opl_Ovar c_PropLog_Opl_Oop_A_N_62
% 0.59/0.61 Problem Properties:
% 0.59/0.61 This is a full first-order problem without equality.
% 0.59/0.61
% 0.59/0.61 After reduction: Problem Properties:
% 0.59/0.61 This is a full first-order problem without equality.
% 0.59/0.61
% 0.59/0.61
% 0.59/0.61 Reduced Input Clauses:
% 0.59/0.61
% 0.59/0.61 Most General Atoms: c_lessequals(c_minus(x0,x1,tc_set(x2)),c_insert(x3,c_minus(x0,c_insert(x3,x1,x2),tc_set(x2)),x2),tc_set(x2)) c_lessequals(c_minus(c_insert(x0,c_minus(x1,c_insert(x2,c_emptyset,x3),tc_set(x3)),x3),x4,tc_set(x3)),c_insert(x0,c_minus(x1,c_insert(x2,x4,x3),tc_set(x3)),x3),tc_set(x3)) c_lessequals(x1,x3,tc_set(tc_PropLog_Opl(x2))) c_in(x0,c_PropLog_Othms(x3,x2),tc_PropLog_Opl(x2))
% 0.59/0.61
% 0.59/0.61 === Starting SPASS-SCL-FOL A Little Less Naive, considering 28 atoms initially, heuristics mode: resolution_1 ===
% 0.59/0.61
% 0.59/0.61 === Backtracking. Learning clause 9:2:2:[6.1,7.1]:TopTop: c_lessequals(c_minus(c_PropLog_Ohyps(v_p,x0,t_a),v_F,tc_set(tc_PropLog_Opl(t_a))),x1,tc_set(tc_PropLog_Opl(t_a))) -> c_in(v_p,c_PropLog_Othms(x1,t_a),tc_PropLog_Opl(t_a))
% 0.59/0.61 === Backtracking. Learning clause 10:2:2:[1.1,7.1]:TopTop: c_lessequals(c_PropLog_Ohyps(v_p,x0,t_a),x1,tc_set(tc_PropLog_Opl(t_a))) -> c_in(v_p,c_PropLog_Othms(c_minus(x1,v_F,tc_set(tc_PropLog_Opl(t_a))),t_a),tc_PropLog_Opl(t_a))
% 0.59/0.61 === Backtracking. Learning clause 11:2:1:[1.3,8.1]:Top: c_in(v_p,c_PropLog_Othms(c_minus(x0,c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(v_v,t_a),c_PropLog_Opl_Ofalse,t_a),v_F,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),t_a),tc_PropLog_Opl(t_a)),c_lessequals(x0,c_PropLog_Ohyps(v_p,v_t,t_a),tc_set(tc_PropLog_Opl(t_a))) ->
% 0.59/0.61 === Backtracking. Learning clause 12:2:6:[1.2,2.1]:TopTopTopTopTopTop: c_in(x0,c_PropLog_Othms(c_minus(c_PropLog_Ohyps(x1,c_insert(x2,x3,x4),x4),x5,tc_set(tc_PropLog_Opl(x4))),x4),tc_PropLog_Opl(x4)) -> c_in(x0,c_PropLog_Othms(c_minus(c_insert(c_PropLog_Opl_Ovar(x2,x4),c_minus(c_PropLog_Ohyps(x1,x3,x4),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x2,x4),c_PropLog_Opl_Ofalse,x4),c_emptyset,tc_PropLog_Opl(x4)),tc_set(tc_PropLog_Opl(x4))),tc_PropLog_Opl(x4)),x5,tc_set(tc_PropLog_Opl(x4))),x4),tc_PropLog_Opl(x4))
% 0.59/0.61 === Backtracking. Learning clause 13:2:5:[6.2,2.1]:TopTopTopTopTop: c_in(x0,c_PropLog_Othms(c_PropLog_Ohyps(x1,c_insert(x2,x3,x4),x4),x4),tc_PropLog_Opl(x4)) -> c_in(x0,c_PropLog_Othms(c_insert(c_PropLog_Opl_Ovar(x2,x4),c_minus(c_PropLog_Ohyps(x1,x3,x4),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x2,x4),c_PropLog_Opl_Ofalse,x4),c_emptyset,tc_PropLog_Opl(x4)),tc_set(tc_PropLog_Opl(x4))),tc_PropLog_Opl(x4)),x4),tc_PropLog_Opl(x4))
% 0.59/0.61 === Backtracking. Learning clause 14:2:7:[1.2,4.1]:TopTopTopTopTopTopTop: c_in(x0,c_PropLog_Othms(c_minus(c_minus(c_insert(x1,c_minus(x2,c_insert(x3,c_emptyset,tc_PropLog_Opl(x4)),tc_set(tc_PropLog_Opl(x4))),tc_PropLog_Opl(x4)),x5,tc_set(tc_PropLog_Opl(x4))),x6,tc_set(tc_PropLog_Opl(x4))),x4),tc_PropLog_Opl(x4)) -> c_in(x0,c_PropLog_Othms(c_minus(c_insert(x1,c_minus(x2,c_insert(x3,x5,tc_PropLog_Opl(x4)),tc_set(tc_PropLog_Opl(x4))),tc_PropLog_Opl(x4)),x6,tc_set(tc_PropLog_Opl(x4))),x4),tc_PropLog_Opl(x4))
% 0.59/0.61 === Backtracking. Learning clause 15:2:6:[6.2,4.1]:TopTopTopTopTopTop: c_in(x0,c_PropLog_Othms(c_minus(c_insert(x1,c_minus(x2,c_insert(x3,c_emptyset,tc_PropLog_Opl(x4)),tc_set(tc_PropLog_Opl(x4))),tc_PropLog_Opl(x4)),x5,tc_set(tc_PropLog_Opl(x4))),x4),tc_PropLog_Opl(x4)) -> c_in(x0,c_PropLog_Othms(c_insert(x1,c_minus(x2,c_insert(x3,x5,tc_PropLog_Opl(x4)),tc_set(tc_PropLog_Opl(x4))),tc_PropLog_Opl(x4)),x4),tc_PropLog_Opl(x4))
% 0.59/0.61 === Clause set with instances from active satisfied. Growing active. New size: 50
% 0.59/0.61 === Restarting.
% 0.59/0.61 === Backtracking. Learning clause 16:2:5:[6.2,3.1]:TopTopTopTopTop: c_in(x0,c_PropLog_Othms(c_minus(x1,x2,tc_set(tc_PropLog_Opl(x3))),x3),tc_PropLog_Opl(x3)) -> c_in(x0,c_PropLog_Othms(c_insert(x4,c_minus(x1,c_insert(x4,x2,tc_PropLog_Opl(x3)),tc_set(tc_PropLog_Opl(x3))),tc_PropLog_Opl(x3)),x3),tc_PropLog_Opl(x3))
% 0.59/0.61 === Conflict found: 11:2:1:[1.3,8.1]:Top: c_in(v_p,c_PropLog_Othms(c_minus(x0,c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(v_v,t_a),c_PropLog_Opl_Ofalse,t_a),v_F,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),t_a),tc_PropLog_Opl(t_a)),c_lessequals(x0,c_PropLog_Ohyps(v_p,v_t,t_a),tc_set(tc_PropLog_Opl(t_a))) -> {x0 -> c_insert(c_PropLog_Opl_Ovar(c_PropLog_Opl_Ofalse,t_a),c_minus(c_PropLog_Ohyps(c_PropLog_Opl_Ofalse,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(c_PropLog_Opl_Ofalse,t_a),c_PropLog_Opl_Ofalse,t_a),c_emptyset,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a))}
% 0.59/0.61 === Backtracking. Learning clause 17:2:3:[11.1,12.2]:TopTopTop: c_lessequals(c_insert(c_PropLog_Opl_Ovar(x0,t_a),c_minus(c_PropLog_Ohyps(x1,x2,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x0,t_a),c_PropLog_Opl_Ofalse,t_a),c_emptyset,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a)),c_PropLog_Ohyps(v_p,v_t,t_a),tc_set(tc_PropLog_Opl(t_a))),c_in(v_p,c_PropLog_Othms(c_minus(c_PropLog_Ohyps(x1,c_insert(x0,x2,t_a),t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(v_v,t_a),c_PropLog_Opl_Ofalse,t_a),v_F,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),t_a),tc_PropLog_Opl(t_a)) ->
% 0.59/0.61 === Clause set with instances from active satisfied. Growing active. New size: 54
% 0.59/0.61 === Restarting.
% 0.59/0.61 === Backtracking. Learning clause 18:3:2:[6.3,11.1]:TopTop: c_in(v_p,c_PropLog_Othms(x0,t_a),tc_PropLog_Opl(t_a)),c_lessequals(x0,c_minus(x1,c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(v_v,t_a),c_PropLog_Opl_Ofalse,t_a),v_F,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_set(tc_PropLog_Opl(t_a))),c_lessequals(x1,c_PropLog_Ohyps(v_p,v_t,t_a),tc_set(tc_PropLog_Opl(t_a))) ->
% 0.59/0.61 === Conflict found: 10:2:2:[1.1,7.1]:TopTop: c_lessequals(c_PropLog_Ohyps(v_p,x0,t_a),x1,tc_set(tc_PropLog_Opl(t_a))) -> c_in(v_p,c_PropLog_Othms(c_minus(x1,v_F,tc_set(tc_PropLog_Opl(t_a))),t_a),tc_PropLog_Opl(t_a)) {x0 -> c_PropLog_Opl_Ofalse, x1 -> c_minus(c_insert(c_PropLog_Opl_Ofalse,c_minus(c_PropLog_Opl_Ofalse,c_insert(c_PropLog_Opl_Ofalse,c_emptyset,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a)),c_PropLog_Opl_Ofalse,tc_set(tc_PropLog_Opl(t_a)))}
% 0.59/0.61 === Backtracking. Learning clause 19:2:5:[10.2,14.1]:TopTopTopTopTop: c_lessequals(c_PropLog_Ohyps(v_p,x0,t_a),c_minus(c_insert(x1,c_minus(x2,c_insert(x3,c_emptyset,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a)),x4,tc_set(tc_PropLog_Opl(t_a))),tc_set(tc_PropLog_Opl(t_a))) -> c_in(v_p,c_PropLog_Othms(c_minus(c_insert(x1,c_minus(x2,c_insert(x3,x4,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a)),v_F,tc_set(tc_PropLog_Opl(t_a))),t_a),tc_PropLog_Opl(t_a))
% 0.59/0.61 === Backtracking. Learning clause 20:3:7:[1.1,12.2]:TopTopTopTopTopTopTop: c_lessequals(c_insert(c_PropLog_Opl_Ovar(x0,x1),c_minus(c_PropLog_Ohyps(x2,x3,x1),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x0,x1),c_PropLog_Opl_Ofalse,x1),c_emptyset,tc_PropLog_Opl(x1)),tc_set(tc_PropLog_Opl(x1))),tc_PropLog_Opl(x1)),x4,tc_set(tc_PropLog_Opl(x1))),c_in(x5,c_PropLog_Othms(c_minus(c_PropLog_Ohyps(x2,c_insert(x0,x3,x1),x1),x6,tc_set(tc_PropLog_Opl(x1))),x1),tc_PropLog_Opl(x1)) -> c_in(x5,c_PropLog_Othms(c_minus(x4,x6,tc_set(tc_PropLog_Opl(x1))),x1),tc_PropLog_Opl(x1))
% 0.59/0.61 === Conflict found: 10:2:2:[1.1,7.1]:TopTop: c_lessequals(c_PropLog_Ohyps(v_p,x0,t_a),x1,tc_set(tc_PropLog_Opl(t_a))) -> c_in(v_p,c_PropLog_Othms(c_minus(x1,v_F,tc_set(tc_PropLog_Opl(t_a))),t_a),tc_PropLog_Opl(t_a)) {x0 -> c_insert(c_PropLog_Opl_Ofalse,c_PropLog_Opl_Ofalse,t_a), x1 -> c_insert(c_PropLog_Opl_Ovar(c_PropLog_Opl_Ofalse,t_a),c_minus(c_PropLog_Ohyps(v_p,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(c_PropLog_Opl_Ofalse,t_a),c_PropLog_Opl_Ofalse,t_a),c_emptyset,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a))}
% 0.59/0.61 === Backtracking. Learning clause 21:1:2:[10.1,2.1]:TopTop: -> c_in(v_p,c_PropLog_Othms(c_minus(c_insert(c_PropLog_Opl_Ovar(x0,t_a),c_minus(c_PropLog_Ohyps(v_p,x1,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x0,t_a),c_PropLog_Opl_Ofalse,t_a),c_emptyset,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a)),v_F,tc_set(tc_PropLog_Opl(t_a))),t_a),tc_PropLog_Opl(t_a))
% 0.59/0.61 === Clause set with instances from active satisfied. Growing active. New size: 57
% 0.59/0.61 === Restarting.
% 0.59/0.61 === Backtracking. Learning clause 22:3:5:[5.2,16.2]:TopTopTopTopTop: c_in(x0,c_PropLog_Othms(c_insert(x1,c_minus(x2,c_insert(c_PropLog_Opl_Oop_A_N_62(x1,c_PropLog_Opl_Ofalse,x3),x4,tc_PropLog_Opl(x3)),tc_set(tc_PropLog_Opl(x3))),tc_PropLog_Opl(x3)),x3),tc_PropLog_Opl(x3)),c_in(x0,c_PropLog_Othms(c_minus(x2,x4,tc_set(tc_PropLog_Opl(x3))),x3),tc_PropLog_Opl(x3)) -> c_in(x0,c_PropLog_Othms(c_minus(x2,c_insert(c_PropLog_Opl_Oop_A_N_62(x1,c_PropLog_Opl_Ofalse,x3),x4,tc_PropLog_Opl(x3)),tc_set(tc_PropLog_Opl(x3))),x3),tc_PropLog_Opl(x3))
% 0.59/0.61 === Clause set with instances from active satisfied. Growing active. New size: 60
% 0.59/0.61 === Restarting.
% 0.59/0.61 === Conflict found: 10:2:2:[1.1,7.1]:TopTop: c_lessequals(c_PropLog_Ohyps(v_p,x0,t_a),x1,tc_set(tc_PropLog_Opl(t_a))) -> c_in(v_p,c_PropLog_Othms(c_minus(x1,v_F,tc_set(tc_PropLog_Opl(t_a))),t_a),tc_PropLog_Opl(t_a)) {x0 -> c_PropLog_Opl_Ofalse, x1 -> c_insert(c_PropLog_Opl_Ofalse,c_minus(c_PropLog_Opl_Ofalse,c_insert(c_PropLog_Opl_Ofalse,c_emptyset,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a))}
% 0.59/0.61 === Backtracking. Learning clause 23:2:4:[10.2,15.1]:TopTopTopTop: c_lessequals(c_PropLog_Ohyps(v_p,x0,t_a),c_insert(x1,c_minus(x2,c_insert(x3,c_emptyset,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))) -> c_in(v_p,c_PropLog_Othms(c_insert(x1,c_minus(x2,c_insert(x3,v_F,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a))
% 0.59/0.61 === Conflict found: 15:2:6:[6.2,4.1]:TopTopTopTopTopTop: c_in(x0,c_PropLog_Othms(c_minus(c_insert(x1,c_minus(x2,c_insert(x3,c_emptyset,tc_PropLog_Opl(x4)),tc_set(tc_PropLog_Opl(x4))),tc_PropLog_Opl(x4)),x5,tc_set(tc_PropLog_Opl(x4))),x4),tc_PropLog_Opl(x4)) -> c_in(x0,c_PropLog_Othms(c_insert(x1,c_minus(x2,c_insert(x3,x5,tc_PropLog_Opl(x4)),tc_set(tc_PropLog_Opl(x4))),tc_PropLog_Opl(x4)),x4),tc_PropLog_Opl(x4)) {x0 -> c_PropLog_Opl_Ofalse, x1 -> c_PropLog_Opl_Ovar(c_PropLog_Opl_Ofalse,c_PropLog_Opl_Ofalse), x2 -> c_PropLog_Ohyps(c_PropLog_Opl_Ofalse,c_PropLog_Opl_Ofalse,c_PropLog_Opl_Ofalse), x3 -> c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(c_PropLog_Opl_Ofalse,c_PropLog_Opl_Ofalse),c_PropLog_Opl_Ofalse,c_PropLog_Opl_Ofalse), x4 -> c_PropLog_Opl_Ofalse, x5 -> c_PropLog_Opl_Ofalse}
% 0.59/0.61 === Backtracking. Learning clause 24:2:6:[15.1,12.2]:TopTopTopTopTopTop: c_in(x0,c_PropLog_Othms(c_minus(c_PropLog_Ohyps(x1,c_insert(x2,x3,x4),x4),x5,tc_set(tc_PropLog_Opl(x4))),x4),tc_PropLog_Opl(x4)) -> c_in(x0,c_PropLog_Othms(c_insert(c_PropLog_Opl_Ovar(x2,x4),c_minus(c_PropLog_Ohyps(x1,x3,x4),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x2,x4),c_PropLog_Opl_Ofalse,x4),x5,tc_PropLog_Opl(x4)),tc_set(tc_PropLog_Opl(x4))),tc_PropLog_Opl(x4)),x4),tc_PropLog_Opl(x4))
% 0.59/0.61 === Backtracking. Learning clause 25:2:3:[1.1,21.1]:TopTopTop: c_lessequals(c_insert(c_PropLog_Opl_Ovar(x0,t_a),c_minus(c_PropLog_Ohyps(v_p,x1,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x0,t_a),c_PropLog_Opl_Ofalse,t_a),c_emptyset,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a)),x2,tc_set(tc_PropLog_Opl(t_a))) -> c_in(v_p,c_PropLog_Othms(c_minus(x2,v_F,tc_set(tc_PropLog_Opl(t_a))),t_a),tc_PropLog_Opl(t_a))
% 0.59/0.61 === Clause set with instances from active satisfied. Growing active. New size: 63
% 0.59/0.61 === Restarting.
% 0.59/0.61 === Backtracking. Learning clause 26:3:6:[6.1,16.2]:TopTopTopTopTopTop: c_lessequals(c_insert(x0,c_minus(x1,c_insert(x0,x2,tc_PropLog_Opl(x3)),tc_set(tc_PropLog_Opl(x3))),tc_PropLog_Opl(x3)),x4,tc_set(tc_PropLog_Opl(x3))),c_in(x5,c_PropLog_Othms(c_minus(x1,x2,tc_set(tc_PropLog_Opl(x3))),x3),tc_PropLog_Opl(x3)) -> c_in(x5,c_PropLog_Othms(x4,x3),tc_PropLog_Opl(x3))
% 0.59/0.61 === Backtracking. Learning clause 27:2:1:[6.3,8.1]:Top: c_in(v_p,c_PropLog_Othms(x0,t_a),tc_PropLog_Opl(t_a)),c_lessequals(x0,c_minus(c_PropLog_Ohyps(v_p,v_t,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(v_v,t_a),c_PropLog_Opl_Ofalse,t_a),v_F,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_set(tc_PropLog_Opl(t_a))) ->
% 0.59/0.61 === Conflict found: 15:2:6:[6.2,4.1]:TopTopTopTopTopTop: c_in(x0,c_PropLog_Othms(c_minus(c_insert(x1,c_minus(x2,c_insert(x3,c_emptyset,tc_PropLog_Opl(x4)),tc_set(tc_PropLog_Opl(x4))),tc_PropLog_Opl(x4)),x5,tc_set(tc_PropLog_Opl(x4))),x4),tc_PropLog_Opl(x4)) -> c_in(x0,c_PropLog_Othms(c_insert(x1,c_minus(x2,c_insert(x3,x5,tc_PropLog_Opl(x4)),tc_set(tc_PropLog_Opl(x4))),tc_PropLog_Opl(x4)),x4),tc_PropLog_Opl(x4)) {x0 -> v_p, x1 -> c_PropLog_Opl_Ovar(c_PropLog_Opl_Ofalse,t_a), x2 -> c_PropLog_Ohyps(v_p,c_PropLog_Opl_Ofalse,t_a), x3 -> c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(c_PropLog_Opl_Ofalse,t_a),c_PropLog_Opl_Ofalse,t_a), x4 -> t_a, x5 -> v_F}
% 0.59/0.61 === Backtracking. Learning clause 28:1:2:[15.1,21.1]:TopTop: -> c_in(v_p,c_PropLog_Othms(c_insert(c_PropLog_Opl_Ovar(x0,t_a),c_minus(c_PropLog_Ohyps(v_p,x1,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x0,t_a),c_PropLog_Opl_Ofalse,t_a),v_F,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a))
% 0.59/0.61 === Clause set with instances from active satisfied. Growing active. New size: 65
% 0.59/0.61 === Restarting.
% 0.59/0.61 === Backtracking. Learning clause 29:3:7:[6.3,15.1]:TopTopTopTopTopTopTop: c_in(x0,c_PropLog_Othms(x1,x2),tc_PropLog_Opl(x2)),c_lessequals(x1,c_minus(c_insert(x3,c_minus(x4,c_insert(x5,c_emptyset,tc_PropLog_Opl(x2)),tc_set(tc_PropLog_Opl(x2))),tc_PropLog_Opl(x2)),x6,tc_set(tc_PropLog_Opl(x2))),tc_set(tc_PropLog_Opl(x2))) -> c_in(x0,c_PropLog_Othms(c_insert(x3,c_minus(x4,c_insert(x5,x6,tc_PropLog_Opl(x2)),tc_set(tc_PropLog_Opl(x2))),tc_PropLog_Opl(x2)),x2),tc_PropLog_Opl(x2))
% 0.59/0.61 === Conflict found: 22:3:5:[5.2,16.2]:TopTopTopTopTop: c_in(x0,c_PropLog_Othms(c_insert(x1,c_minus(x2,c_insert(c_PropLog_Opl_Oop_A_N_62(x1,c_PropLog_Opl_Ofalse,x3),x4,tc_PropLog_Opl(x3)),tc_set(tc_PropLog_Opl(x3))),tc_PropLog_Opl(x3)),x3),tc_PropLog_Opl(x3)),c_in(x0,c_PropLog_Othms(c_minus(x2,x4,tc_set(tc_PropLog_Opl(x3))),x3),tc_PropLog_Opl(x3)) -> c_in(x0,c_PropLog_Othms(c_minus(x2,c_insert(c_PropLog_Opl_Oop_A_N_62(x1,c_PropLog_Opl_Ofalse,x3),x4,tc_PropLog_Opl(x3)),tc_set(tc_PropLog_Opl(x3))),x3),tc_PropLog_Opl(x3)) {x0 -> c_PropLog_Opl_Ofalse, x1 -> c_PropLog_Opl_Ovar(c_PropLog_Opl_Ofalse,c_PropLog_Opl_Ofalse), x2 -> c_PropLog_Ohyps(c_PropLog_Opl_Ofalse,c_PropLog_Opl_Ofalse,c_PropLog_Opl_Ofalse), x3 -> c_PropLog_Opl_Ofalse, x4 -> c_emptyset}
% 0.59/0.61 === Backtracking. Learning clause 30:3:5:[22.1,13.2]:TopTopTopTopTop: c_in(x0,c_PropLog_Othms(c_minus(c_PropLog_Ohyps(x1,x2,x3),c_emptyset,tc_set(tc_PropLog_Opl(x3))),x3),tc_PropLog_Opl(x3)),c_in(x0,c_PropLog_Othms(c_PropLog_Ohyps(x1,c_insert(x4,x2,x3),x3),x3),tc_PropLog_Opl(x3)) -> c_in(x0,c_PropLog_Othms(c_minus(c_PropLog_Ohyps(x1,x2,x3),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x4,x3),c_PropLog_Opl_Ofalse,x3),c_emptyset,tc_PropLog_Opl(x3)),tc_set(tc_PropLog_Opl(x3))),x3),tc_PropLog_Opl(x3))
% 0.59/0.61 === Conflict found: 22:3:5:[5.2,16.2]:TopTopTopTopTop: c_in(x0,c_PropLog_Othms(c_insert(x1,c_minus(x2,c_insert(c_PropLog_Opl_Oop_A_N_62(x1,c_PropLog_Opl_Ofalse,x3),x4,tc_PropLog_Opl(x3)),tc_set(tc_PropLog_Opl(x3))),tc_PropLog_Opl(x3)),x3),tc_PropLog_Opl(x3)),c_in(x0,c_PropLog_Othms(c_minus(x2,x4,tc_set(tc_PropLog_Opl(x3))),x3),tc_PropLog_Opl(x3)) -> c_in(x0,c_PropLog_Othms(c_minus(x2,c_insert(c_PropLog_Opl_Oop_A_N_62(x1,c_PropLog_Opl_Ofalse,x3),x4,tc_PropLog_Opl(x3)),tc_set(tc_PropLog_Opl(x3))),x3),tc_PropLog_Opl(x3)) {x0 -> v_p, x1 -> c_PropLog_Opl_Ovar(c_PropLog_Opl_Ofalse,t_a), x2 -> c_PropLog_Ohyps(v_p,c_PropLog_Opl_Ofalse,t_a), x3 -> t_a, x4 -> v_F}
% 0.59/0.61 === Backtracking. Learning clause 32:1:2:[7.0,31.0,22.1,28.1]:TopTop: -> c_in(v_p,c_PropLog_Othms(c_minus(c_PropLog_Ohyps(v_p,x0,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x1,t_a),c_PropLog_Opl_Ofalse,t_a),v_F,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),t_a),tc_PropLog_Opl(t_a))
% 0.59/0.61 === Conflict found: 32:1:2:[7.0,31.0,22.1,28.1]:TopTop: -> c_in(v_p,c_PropLog_Othms(c_minus(c_PropLog_Ohyps(v_p,x0,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x1,t_a),c_PropLog_Opl_Ofalse,t_a),v_F,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),t_a),tc_PropLog_Opl(t_a)) {x0 -> v_t, x1 -> v_v}
% 0.59/0.61
% 0.59/0.61 SZS status Unsatisfiable
% 0.59/0.61
% 0.59/0.61 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.59/0.61
% 0.59/0.61 SPASS-SCL-FOL Statistics:
% 0.59/0.61 Number of learned clauses: 23
% 0.59/0.61 Number of propagations: 350
% 0.59/0.61 Number of decisions: 549
% 0.59/0.61 Number of resolutions: 24
% 0.59/0.61 Number of condensations: 0
% 0.59/0.61 Number of sub resolutions: 1
% 0.59/0.61 Number of input literals (deduplicated): 10
% 0.59/0.61 Number of grows: 6
% 0.59/0.61 Number of considered ground atoms: 65
% 0.59/0.61
% 0.59/0.61 Needed: 0:00:00.09
% 0.59/0.61
%------------------------------------------------------------------------------