%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : LCL429-2 : TPTP v9.2.1. Released v3.2.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 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 : Thu May 7 07:27:50 PM UTC 2026
% Result : Unsatisfiable 0.51s 0.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : LCL429-2 : TPTP v9.2.1. Released v3.2.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n007.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Thu May 7 12:32:09 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.51/0.59 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.51/0.59 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.51/0.59 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.51/0.59 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.51/0.59 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.51/0.59 Execution resolution_1 ended with status: unsatisfiable
% 0.51/0.59 Used heuristic: resolution_1
% 0.51/0.59
% 0.51/0.59 Input Clauses:
% 0.51/0.59
% 0.51/0.59 Predicates: c_in c_lessequals
% 0.51/0.59 Fol Constants: c_emptyset c_PropLog_Opl_Ofalse v_p t_a v_F v_t v_v
% 0.51/0.59 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.51/0.59 Problem Properties:
% 0.51/0.59 This is a full first-order problem without equality.
% 0.51/0.59
% 0.51/0.59 After reduction: Problem Properties:
% 0.51/0.59 This is a full first-order problem without equality.
% 0.51/0.59
% 0.51/0.59
% 0.51/0.59 Reduced Input Clauses:
% 0.51/0.59
% 0.51/0.59 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.51/0.59
% 0.51/0.59 === Starting SPASS-SCL-FOL A Little Less Naive, considering 27 atoms initially, heuristics mode: resolution_1 ===
% 0.51/0.59
% 0.51/0.59 === 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.51/0.59 === 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.51/0.59 === 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_Ovar(v_v,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.51/0.59 === Backtracking. Learning clause 12: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.51/0.59 === Backtracking. Learning clause 13:2:6:[1.2,2.1]:TopTopTopTopTopTop: c_in(x0,c_PropLog_Othms(c_minus(c_PropLog_Ohyps(x1,c_minus(x2,c_insert(x3,c_emptyset,x4),tc_set(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_Oop_A_N_62(c_PropLog_Opl_Ovar(x3,x4),c_PropLog_Opl_Ofalse,x4),c_minus(c_PropLog_Ohyps(x1,x2,x4),c_insert(c_PropLog_Opl_Ovar(x3,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.51/0.59 === Backtracking. Learning clause 14:2:5:[6.2,2.1]:TopTopTopTopTop: c_in(x0,c_PropLog_Othms(c_PropLog_Ohyps(x1,c_minus(x2,c_insert(x3,c_emptyset,x4),tc_set(x4)),x4),x4),tc_PropLog_Opl(x4)) -> c_in(x0,c_PropLog_Othms(c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x3,x4),c_PropLog_Opl_Ofalse,x4),c_minus(c_PropLog_Ohyps(x1,x2,x4),c_insert(c_PropLog_Opl_Ovar(x3,x4),c_emptyset,tc_PropLog_Opl(x4)),tc_set(tc_PropLog_Opl(x4))),tc_PropLog_Opl(x4)),x4),tc_PropLog_Opl(x4))
% 0.51/0.59 === Clause set with instances from active satisfied. Growing active. New size: 46
% 0.51/0.59 === Restarting.
% 0.51/0.59 === 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_emptyset, x1 -> c_minus(c_insert(c_emptyset,c_minus(c_emptyset,c_insert(c_emptyset,c_emptyset,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a)),c_emptyset,tc_set(tc_PropLog_Opl(t_a)))}
% 0.51/0.59 === Backtracking. Learning clause 15:2:5:[10.2,12.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.51/0.59 === 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_minus(c_emptyset,c_insert(c_emptyset,c_emptyset,t_a),tc_set(t_a)), x1 -> c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(c_emptyset,t_a),c_PropLog_Opl_Ofalse,t_a),c_minus(c_PropLog_Ohyps(v_p,c_emptyset,t_a),c_insert(c_PropLog_Opl_Ovar(c_emptyset,t_a),c_emptyset,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a))}
% 0.51/0.59 === Backtracking. Learning clause 16:1:2:[10.1,2.1]:TopTop: -> c_in(v_p,c_PropLog_Othms(c_minus(c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x0,t_a),c_PropLog_Opl_Ofalse,t_a),c_minus(c_PropLog_Ohyps(v_p,x1,t_a),c_insert(c_PropLog_Opl_Ovar(x0,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.51/0.59 === 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_Ovar(v_v,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_Oop_A_N_62(c_PropLog_Opl_Ovar(c_emptyset,t_a),c_PropLog_Opl_Ofalse,t_a),c_minus(c_PropLog_Ohyps(c_emptyset,c_emptyset,t_a),c_insert(c_PropLog_Opl_Ovar(c_emptyset,t_a),c_emptyset,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a))}
% 0.51/0.59 === Backtracking. Learning clause 17:2:3:[11.1,13.2]:TopTopTop: c_lessequals(c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x0,t_a),c_PropLog_Opl_Ofalse,t_a),c_minus(c_PropLog_Ohyps(x1,x2,t_a),c_insert(c_PropLog_Opl_Ovar(x0,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_minus(x2,c_insert(x0,c_emptyset,t_a),tc_set(t_a)),t_a),c_insert(c_PropLog_Opl_Ovar(v_v,t_a),v_F,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),t_a),tc_PropLog_Opl(t_a)) ->
% 0.51/0.59 === Clause set with instances from active satisfied. Growing active. New size: 48
% 0.51/0.59 === Restarting.
% 0.51/0.59 === Conflict found: 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)) {x0 -> c_emptyset, x1 -> c_insert(c_emptyset,c_minus(c_PropLog_Ohyps(v_p,c_emptyset,t_a),c_insert(c_emptyset,v_F,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a))}
% 0.51/0.59 === Backtracking. Learning clause 18:1:2:[9.1,3.1]:TopTop: -> c_in(v_p,c_PropLog_Othms(c_insert(x0,c_minus(c_PropLog_Ohyps(v_p,x1,t_a),c_insert(x0,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.51/0.59 === Backtracking. Learning clause 19:2:3:[1.1,16.1]:TopTopTop: c_lessequals(c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x0,t_a),c_PropLog_Opl_Ofalse,t_a),c_minus(c_PropLog_Ohyps(v_p,x1,t_a),c_insert(c_PropLog_Opl_Ovar(x0,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.51/0.59 === Backtracking. Learning clause 20:2:3:[6.1,16.1]:TopTopTop: c_lessequals(c_minus(c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x0,t_a),c_PropLog_Opl_Ofalse,t_a),c_minus(c_PropLog_Ohyps(v_p,x1,t_a),c_insert(c_PropLog_Opl_Ovar(x0,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))),x2,tc_set(tc_PropLog_Opl(t_a))) -> c_in(v_p,c_PropLog_Othms(x2,t_a),tc_PropLog_Opl(t_a))
% 0.51/0.59 === Clause set with instances from active satisfied. Growing active. New size: 56
% 0.51/0.59 === Restarting.
% 0.51/0.59 === Conflict found: 20:2:3:[6.1,16.1]:TopTopTop: c_lessequals(c_minus(c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x0,t_a),c_PropLog_Opl_Ofalse,t_a),c_minus(c_PropLog_Ohyps(v_p,x1,t_a),c_insert(c_PropLog_Opl_Ovar(x0,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))),x2,tc_set(tc_PropLog_Opl(t_a))) -> c_in(v_p,c_PropLog_Othms(x2,t_a),tc_PropLog_Opl(t_a)) {x0 -> c_emptyset, x1 -> c_emptyset, x2 -> c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(c_emptyset,t_a),c_PropLog_Opl_Ofalse,t_a),c_minus(c_PropLog_Ohyps(v_p,c_emptyset,t_a),c_insert(c_PropLog_Opl_Ovar(c_emptyset,t_a),v_F,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a))}
% 0.51/0.59 === Backtracking. Learning clause 21:1:2:[20.1,4.1]:TopTop: -> c_in(v_p,c_PropLog_Othms(c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x0,t_a),c_PropLog_Opl_Ofalse,t_a),c_minus(c_PropLog_Ohyps(v_p,x1,t_a),c_insert(c_PropLog_Opl_Ovar(x0,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.51/0.59 === Conflict found: 20:2:3:[6.1,16.1]:TopTopTop: c_lessequals(c_minus(c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x0,t_a),c_PropLog_Opl_Ofalse,t_a),c_minus(c_PropLog_Ohyps(v_p,x1,t_a),c_insert(c_PropLog_Opl_Ovar(x0,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))),x2,tc_set(tc_PropLog_Opl(t_a))) -> c_in(v_p,c_PropLog_Othms(x2,t_a),tc_PropLog_Opl(t_a)) {x0 -> c_emptyset, x1 -> c_emptyset, x2 -> c_insert(c_emptyset,c_minus(c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(c_emptyset,t_a),c_PropLog_Opl_Ofalse,t_a),c_minus(c_PropLog_Ohyps(v_p,c_emptyset,t_a),c_insert(c_PropLog_Opl_Ovar(c_emptyset,t_a),c_emptyset,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a)),c_insert(c_emptyset,v_F,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a))}
% 0.51/0.59 === Backtracking. Learning clause 22:1:3:[20.1,3.1]:TopTopTop: -> c_in(v_p,c_PropLog_Othms(c_insert(x0,c_minus(c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Ovar(x1,t_a),c_PropLog_Opl_Ofalse,t_a),c_minus(c_PropLog_Ohyps(v_p,x2,t_a),c_insert(c_PropLog_Opl_Ovar(x1,t_a),c_emptyset,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_PropLog_Opl(t_a)),c_insert(x0,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.51/0.59 === Clause set with instances from active satisfied. Growing active. New size: 63
% 0.51/0.59 === Restarting.
% 0.51/0.59 === Backtracking. Learning clause 23: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_Ovar(v_v,t_a),v_F,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),tc_set(tc_PropLog_Opl(t_a))) ->
% 0.51/0.59 === Backtracking. Learning clause 24:2:2:[5.2,18.1]:TopTop: c_in(v_p,c_PropLog_Othms(c_insert(x0,c_minus(c_PropLog_Ohyps(v_p,x1,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(x0,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)) -> c_in(v_p,c_PropLog_Othms(c_minus(c_PropLog_Ohyps(v_p,x1,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(x0,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.51/0.59 === Clause set with instances from active satisfied. Growing active. New size: 64
% 0.51/0.59 === Restarting.
% 0.51/0.59 === Backtracking. Learning clause 25:2:3:[6.1,18.1]:TopTopTop: c_lessequals(c_insert(x0,c_minus(c_PropLog_Ohyps(v_p,x1,t_a),c_insert(x0,v_F,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(x2,t_a),tc_PropLog_Opl(t_a))
% 0.51/0.59 === Backtracking. Learning clause 26:1:2:[5.2,21.1,18.1]:TopTop: -> c_in(v_p,c_PropLog_Othms(c_minus(c_PropLog_Ohyps(v_p,x0,t_a),c_insert(c_PropLog_Opl_Ovar(x1,t_a),v_F,tc_PropLog_Opl(t_a)),tc_set(tc_PropLog_Opl(t_a))),t_a),tc_PropLog_Opl(t_a))
% 0.51/0.59 === Conflict found: 26:1:2:[5.2,21.1,18.1]:TopTop: -> c_in(v_p,c_PropLog_Othms(c_minus(c_PropLog_Ohyps(v_p,x0,t_a),c_insert(c_PropLog_Opl_Ovar(x1,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.51/0.59
% 0.51/0.59 SZS status Unsatisfiable
% 0.51/0.59
% 0.51/0.59 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.51/0.59
% 0.51/0.59 SPASS-SCL-FOL Statistics:
% 0.51/0.59 Number of learned clauses: 18
% 0.51/0.59 Number of propagations: 264
% 0.51/0.59 Number of decisions: 450
% 0.51/0.59 Number of resolutions: 20
% 0.51/0.59 Number of condensations: 0
% 0.51/0.59 Number of sub resolutions: 0
% 0.51/0.59 Number of input literals (deduplicated): 10
% 0.51/0.59 Number of grows: 5
% 0.51/0.59 Number of considered ground atoms: 64
% 0.51/0.59
% 0.51/0.59 Needed: 0:00:00.06
% 0.51/0.59
%------------------------------------------------------------------------------