%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRA004+1 : TPTP v9.0.0. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n020.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 : Wed Apr 9 06:23:19 PM UTC 2025
% Result : Theorem 5.85s 2.42s
% Output : CNFRefutation 5.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 9
% Syntax : Number of formulae : 81 ( 39 unt; 0 typ; 0 def)
% Number of atoms : 177 ( 43 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 183 ( 87 ~; 61 |; 22 &)
% ( 2 <=>; 9 =>; 1 <=; 1 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 13 ( 11 usr; 2 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 12 con; 0-5 aty)
% Number of variables : 134 ( 130 !; 4 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ triangle > shortest_path > precedes > path > sequential > on_path > less_or_equal > in_path > vertex > edge > path_cons > number_of_in > minus > #nlpp > tail_of > length_of > head_of > triangles > sequential_pairs > n1 > graph > empty > edges > complete > #skF_11 > #skF_6 > #skF_5 > #skF_10 > #skF_14 > #skF_13 > #skF_2 > #skF_9 > #skF_7 > #skF_4 > #skF_3 > #skF_8 > #skF_1 > #skF_12
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(head_of,type,
head_of: $i > $i ).
tff(less_or_equal,type,
less_or_equal: ( $i * $i ) > $o ).
tff(triangle,type,
triangle: ( $i * $i * $i ) > $o ).
tff(triangles,type,
triangles: $i ).
tff('#skF_11',type,
'#skF_11': $i ).
tff('#skF_6',type,
'#skF_6': ( $i * $i * $i ) > $i ).
tff(number_of_in,type,
number_of_in: ( $i * $i ) > $i ).
tff(on_path,type,
on_path: ( $i * $i ) > $o ).
tff('#skF_5',type,
'#skF_5': ( $i * $i * $i * $i * $i ) > $i ).
tff('#skF_10',type,
'#skF_10': $i ).
tff(vertex,type,
vertex: $i > $o ).
tff(n1,type,
n1: $i ).
tff('#skF_14',type,
'#skF_14': $i ).
tff(length_of,type,
length_of: $i > $i ).
tff(sequential_pairs,type,
sequential_pairs: $i ).
tff('#skF_13',type,
'#skF_13': $i ).
tff(edge,type,
edge: $i > $o ).
tff('#skF_2',type,
'#skF_2': ( $i * $i * $i ) > $i ).
tff(precedes,type,
precedes: ( $i * $i * $i ) > $o ).
tff(graph,type,
graph: $i ).
tff('#skF_9',type,
'#skF_9': $i ).
tff('#skF_7',type,
'#skF_7': ( $i * $i * $i ) > $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i * $i * $i ) > $i ).
tff(in_path,type,
in_path: ( $i * $i ) > $o ).
tff(sequential,type,
sequential: ( $i * $i ) > $o ).
tff('#skF_3',type,
'#skF_3': ( $i * $i * $i ) > $i ).
tff(tail_of,type,
tail_of: $i > $i ).
tff(edges,type,
edges: $i ).
tff(complete,type,
complete: $o ).
tff(path_cons,type,
path_cons: ( $i * $i ) > $i ).
tff('#skF_8',type,
'#skF_8': ( $i * $i * $i ) > $i ).
tff(empty,type,
empty: $i ).
tff(shortest_path,type,
shortest_path: ( $i * $i * $i ) > $o ).
tff('#skF_1',type,
'#skF_1': ( $i * $i ) > $i ).
tff('#skF_12',type,
'#skF_12': $i ).
tff(path,type,
path: ( $i * $i * $i ) > $o ).
tff(minus,type,
minus: ( $i * $i ) > $i ).
tff(f_271,negated_conjecture,
~ ! [V1,V2,E1,E2,P] :
( ( shortest_path(V1,V2,P)
& precedes(E1,E2,P) )
=> ( ~ ? [E3] :
( ( tail_of(E3) = tail_of(E1) )
& ( head_of(E3) = head_of(E2) ) )
& ( head_of(E2) != tail_of(E1) )
& ( head_of(E2) != head_of(E1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',shortest_path_properties_lemma) ).
tff(f_189,axiom,
! [P,V1,V2] :
( path(V1,V2,P)
=> ! [E1,E2] :
( precedes(E1,E2,P)
=> ( on_path(E1,P)
& on_path(E2,P)
& ( sequential(E1,E2)
<~> ? [E3] :
( sequential(E1,E3)
& precedes(E3,E2,P) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRA001+0.ax',precedes_properties) ).
tff(f_201,axiom,
! [V1,V2,SP] :
( shortest_path(V1,V2,SP)
<=> ( path(V1,V2,SP)
& ( V1 != V2 )
& ! [P] :
( path(V1,V2,P)
=> less_or_equal(length_of(SP),length_of(P)) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRA001+0.ax',shortest_path_defn) ).
tff(f_133,axiom,
! [V1,V2,P,E] :
( ( path(V1,V2,P)
& on_path(E,P) )
=> ( edge(E)
& in_path(head_of(E),P)
& in_path(tail_of(E),P) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRA001+0.ax',on_path_properties) ).
tff(f_63,axiom,
! [E] :
( edge(E)
=> ( vertex(head_of(E))
& vertex(tail_of(E)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRA001+0.ax',edge_ends_are_vertices) ).
tff(f_157,axiom,
! [E1,E2] :
( sequential(E1,E2)
<=> ( edge(E1)
& edge(E2)
& ( E1 != E2 )
& ( head_of(E1) = tail_of(E2) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRA001+0.ax',sequential_defn) ).
tff(f_173,axiom,
! [P,V1,V2] :
( path(V1,V2,P)
=> ! [E1,E2] :
( precedes(E1,E2,P)
<= ( on_path(E1,P)
& on_path(E2,P)
& ( sequential(E1,E2)
| ? [E3] :
( sequential(E1,E3)
& precedes(E3,E2,P) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRA001+0.ax',precedes_defn) ).
tff(f_214,axiom,
! [V1,V2,E1,E2,P] :
( ( shortest_path(V1,V2,P)
& precedes(E1,E2,P) )
=> ( ~ ? [E3] :
( ( tail_of(E3) = tail_of(E1) )
& ( head_of(E3) = head_of(E2) ) )
& ~ precedes(E2,E1,P) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRA001+0.ax',shortest_path_properties) ).
tff(f_57,axiom,
! [E] :
( edge(E)
=> ( head_of(E) != tail_of(E) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRA001+0.ax',no_loops) ).
tff(c_142,plain,
precedes('#skF_11','#skF_12','#skF_13'),
inference(cnfTransformation,[status(thm)],[f_271]) ).
tff(c_378,plain,
! [V2_235,V1_236,E1_232,P_234,E2_233] :
( on_path(E2_233,P_234)
| ~ precedes(E1_232,E2_233,P_234)
| ~ path(V1_236,V2_235,P_234) ),
inference(cnfTransformation,[status(thm)],[f_189]) ).
tff(c_381,plain,
! [V1_236,V2_235] :
( on_path('#skF_12','#skF_13')
| ~ path(V1_236,V2_235,'#skF_13') ),
inference(resolution,[status(thm)],[c_142,c_378]) ).
tff(c_382,plain,
! [V1_236,V2_235] : ~ path(V1_236,V2_235,'#skF_13'),
inference(splitLeft,[status(thm)],[c_381]) ).
tff(c_144,plain,
shortest_path('#skF_9','#skF_10','#skF_13'),
inference(cnfTransformation,[status(thm)],[f_271]) ).
tff(c_322,plain,
! [V1_207,V2_208,SP_209] :
( path(V1_207,V2_208,SP_209)
| ~ shortest_path(V1_207,V2_208,SP_209) ),
inference(cnfTransformation,[status(thm)],[f_201]) ).
tff(c_326,plain,
path('#skF_9','#skF_10','#skF_13'),
inference(resolution,[status(thm)],[c_144,c_322]) ).
tff(c_384,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_382,c_326]) ).
tff(c_385,plain,
on_path('#skF_12','#skF_13'),
inference(splitRight,[status(thm)],[c_381]) ).
tff(c_62,plain,
! [E_29,P_28,V1_26,V2_27] :
( edge(E_29)
| ~ on_path(E_29,P_28)
| ~ path(V1_26,V2_27,P_28) ),
inference(cnfTransformation,[status(thm)],[f_133]) ).
tff(c_388,plain,
! [V1_26,V2_27] :
( edge('#skF_12')
| ~ path(V1_26,V2_27,'#skF_13') ),
inference(resolution,[status(thm)],[c_385,c_62]) ).
tff(c_390,plain,
! [V1_26,V2_27] : ~ path(V1_26,V2_27,'#skF_13'),
inference(splitLeft,[status(thm)],[c_388]) ).
tff(c_392,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_390,c_326]) ).
tff(c_393,plain,
edge('#skF_12'),
inference(splitRight,[status(thm)],[c_388]) ).
tff(c_148,plain,
( ( tail_of('#skF_11') = tail_of('#skF_14') )
| ( head_of('#skF_11') = head_of('#skF_12') )
| ( tail_of('#skF_11') = head_of('#skF_12') ) ),
inference(cnfTransformation,[status(thm)],[f_271]) ).
tff(c_156,plain,
tail_of('#skF_11') = head_of('#skF_12'),
inference(splitLeft,[status(thm)],[c_148]) ).
tff(c_4,plain,
! [E_2] :
( vertex(tail_of(E_2))
| ~ edge(E_2) ),
inference(cnfTransformation,[status(thm)],[f_63]) ).
tff(c_160,plain,
( vertex(head_of('#skF_12'))
| ~ edge('#skF_11') ),
inference(superposition,[status(thm),theory(equality)],[c_156,c_4]) ).
tff(c_164,plain,
~ edge('#skF_11'),
inference(splitLeft,[status(thm)],[c_160]) ).
tff(c_176,plain,
! [V1_134,V2_135,SP_136] :
( path(V1_134,V2_135,SP_136)
| ~ shortest_path(V1_134,V2_135,SP_136) ),
inference(cnfTransformation,[status(thm)],[f_201]) ).
tff(c_180,plain,
path('#skF_9','#skF_10','#skF_13'),
inference(resolution,[status(thm)],[c_144,c_176]) ).
tff(c_264,plain,
! [E_171,P_172,V1_173,V2_174] :
( in_path(tail_of(E_171),P_172)
| ~ on_path(E_171,P_172)
| ~ path(V1_173,V2_174,P_172) ),
inference(cnfTransformation,[status(thm)],[f_133]) ).
tff(c_268,plain,
! [E_175] :
( in_path(tail_of(E_175),'#skF_13')
| ~ on_path(E_175,'#skF_13') ),
inference(resolution,[status(thm)],[c_180,c_264]) ).
tff(c_276,plain,
( in_path(head_of('#skF_12'),'#skF_13')
| ~ on_path('#skF_11','#skF_13') ),
inference(superposition,[status(thm),theory(equality)],[c_156,c_268]) ).
tff(c_278,plain,
~ on_path('#skF_11','#skF_13'),
inference(splitLeft,[status(thm)],[c_276]) ).
tff(c_279,plain,
! [E1_176,P_178,V2_179,V1_180,E2_177] :
( on_path(E1_176,P_178)
| ~ precedes(E1_176,E2_177,P_178)
| ~ path(V1_180,V2_179,P_178) ),
inference(cnfTransformation,[status(thm)],[f_189]) ).
tff(c_281,plain,
! [V1_180,V2_179] :
( on_path('#skF_11','#skF_13')
| ~ path(V1_180,V2_179,'#skF_13') ),
inference(resolution,[status(thm)],[c_142,c_279]) ).
tff(c_284,plain,
! [V1_180,V2_179] : ~ path(V1_180,V2_179,'#skF_13'),
inference(negUnitSimplification,[status(thm)],[c_278,c_281]) ).
tff(c_286,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_284,c_180]) ).
tff(c_288,plain,
on_path('#skF_11','#skF_13'),
inference(splitRight,[status(thm)],[c_276]) ).
tff(c_290,plain,
! [V1_26,V2_27] :
( edge('#skF_11')
| ~ path(V1_26,V2_27,'#skF_13') ),
inference(resolution,[status(thm)],[c_288,c_62]) ).
tff(c_293,plain,
! [V1_26,V2_27] : ~ path(V1_26,V2_27,'#skF_13'),
inference(negUnitSimplification,[status(thm)],[c_164,c_290]) ).
tff(c_302,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_293,c_180]) ).
tff(c_304,plain,
edge('#skF_11'),
inference(splitRight,[status(thm)],[c_160]) ).
tff(c_70,plain,
! [E1_35,E2_36] :
( sequential(E1_35,E2_36)
| ( tail_of(E2_36) != head_of(E1_35) )
| ( E2_36 = E1_35 )
| ~ edge(E2_36)
| ~ edge(E1_35) ),
inference(cnfTransformation,[status(thm)],[f_157]) ).
tff(c_366,plain,
! [V2_230,V1_231,P_229,E2_228,E1_227] :
( on_path(E1_227,P_229)
| ~ precedes(E1_227,E2_228,P_229)
| ~ path(V1_231,V2_230,P_229) ),
inference(cnfTransformation,[status(thm)],[f_189]) ).
tff(c_369,plain,
! [V1_231,V2_230] :
( on_path('#skF_11','#skF_13')
| ~ path(V1_231,V2_230,'#skF_13') ),
inference(resolution,[status(thm)],[c_142,c_366]) ).
tff(c_370,plain,
! [V1_231,V2_230] : ~ path(V1_231,V2_230,'#skF_13'),
inference(splitLeft,[status(thm)],[c_369]) ).
tff(c_372,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_370,c_326]) ).
tff(c_373,plain,
on_path('#skF_11','#skF_13'),
inference(splitRight,[status(thm)],[c_369]) ).
tff(c_648,plain,
! [E1_305,V1_304,P_306,V2_303,E2_307] :
( ~ sequential(E1_305,E2_307)
| precedes(E1_305,E2_307,P_306)
| ~ on_path(E2_307,P_306)
| ~ on_path(E1_305,P_306)
| ~ path(V1_304,V2_303,P_306) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_658,plain,
! [E1_308,E2_309] :
( ~ sequential(E1_308,E2_309)
| precedes(E1_308,E2_309,'#skF_13')
| ~ on_path(E2_309,'#skF_13')
| ~ on_path(E1_308,'#skF_13') ),
inference(resolution,[status(thm)],[c_326,c_648]) ).
tff(c_453,plain,
! [V2_255,E1_256,V1_253,P_252,E2_254] :
( ~ precedes(E2_254,E1_256,P_252)
| ~ precedes(E1_256,E2_254,P_252)
| ~ shortest_path(V1_253,V2_255,P_252) ),
inference(cnfTransformation,[status(thm)],[f_214]) ).
tff(c_456,plain,
! [V1_253,V2_255] :
( ~ precedes('#skF_12','#skF_11','#skF_13')
| ~ shortest_path(V1_253,V2_255,'#skF_13') ),
inference(resolution,[status(thm)],[c_142,c_453]) ).
tff(c_457,plain,
~ precedes('#skF_12','#skF_11','#skF_13'),
inference(splitLeft,[status(thm)],[c_456]) ).
tff(c_663,plain,
( ~ sequential('#skF_12','#skF_11')
| ~ on_path('#skF_11','#skF_13')
| ~ on_path('#skF_12','#skF_13') ),
inference(resolution,[status(thm)],[c_658,c_457]) ).
tff(c_673,plain,
~ sequential('#skF_12','#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_385,c_373,c_663]) ).
tff(c_679,plain,
( ( tail_of('#skF_11') != head_of('#skF_12') )
| ( '#skF_11' = '#skF_12' )
| ~ edge('#skF_11')
| ~ edge('#skF_12') ),
inference(resolution,[status(thm)],[c_70,c_673]) ).
tff(c_682,plain,
'#skF_11' = '#skF_12',
inference(demodulation,[status(thm),theory(equality)],[c_393,c_304,c_156,c_679]) ).
tff(c_308,plain,
! [E_190] :
( ( tail_of(E_190) != head_of(E_190) )
| ~ edge(E_190) ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_311,plain,
tail_of('#skF_11') != head_of('#skF_11'),
inference(resolution,[status(thm)],[c_304,c_308]) ).
tff(c_313,plain,
head_of('#skF_11') != head_of('#skF_12'),
inference(demodulation,[status(thm),theory(equality)],[c_156,c_311]) ).
tff(c_705,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_682,c_313]) ).
tff(c_706,plain,
! [V1_253,V2_255] : ~ shortest_path(V1_253,V2_255,'#skF_13'),
inference(splitRight,[status(thm)],[c_456]) ).
tff(c_727,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_706,c_144]) ).
tff(c_729,plain,
tail_of('#skF_11') != head_of('#skF_12'),
inference(splitRight,[status(thm)],[c_148]) ).
tff(c_146,plain,
( ( head_of('#skF_14') = head_of('#skF_12') )
| ( head_of('#skF_11') = head_of('#skF_12') )
| ( tail_of('#skF_11') = head_of('#skF_12') ) ),
inference(cnfTransformation,[status(thm)],[f_271]) ).
tff(c_731,plain,
( ( head_of('#skF_14') = head_of('#skF_12') )
| ( head_of('#skF_11') = head_of('#skF_12') ) ),
inference(negUnitSimplification,[status(thm)],[c_729,c_146]) ).
tff(c_732,plain,
head_of('#skF_11') = head_of('#skF_12'),
inference(splitLeft,[status(thm)],[c_731]) ).
tff(c_1003,plain,
! [E1_465,E2_463,E3_466,V2_464,V1_462,P_461] :
( ( head_of(E3_466) != head_of(E2_463) )
| ( tail_of(E3_466) != tail_of(E1_465) )
| ~ precedes(E1_465,E2_463,P_461)
| ~ shortest_path(V1_462,V2_464,P_461) ),
inference(cnfTransformation,[status(thm)],[f_214]) ).
tff(c_1123,plain,
! [E2_484,V1_483,V2_486,E1_485,P_487] :
( ( head_of(E2_484) != head_of('#skF_12') )
| ( tail_of(E1_485) != tail_of('#skF_11') )
| ~ precedes(E1_485,E2_484,P_487)
| ~ shortest_path(V1_483,V2_486,P_487) ),
inference(superposition,[status(thm),theory(equality)],[c_732,c_1003]) ).
tff(c_1126,plain,
! [V1_483,V2_486] : ~ shortest_path(V1_483,V2_486,'#skF_13'),
inference(resolution,[status(thm)],[c_142,c_1123]) ).
tff(c_1128,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1126,c_144]) ).
tff(c_1130,plain,
head_of('#skF_11') != head_of('#skF_12'),
inference(splitRight,[status(thm)],[c_731]) ).
tff(c_728,plain,
( ( head_of('#skF_11') = head_of('#skF_12') )
| ( tail_of('#skF_11') = tail_of('#skF_14') ) ),
inference(splitRight,[status(thm)],[c_148]) ).
tff(c_1143,plain,
tail_of('#skF_11') = tail_of('#skF_14'),
inference(negUnitSimplification,[status(thm)],[c_1130,c_728]) ).
tff(c_1129,plain,
head_of('#skF_14') = head_of('#skF_12'),
inference(splitRight,[status(thm)],[c_731]) ).
tff(c_1423,plain,
! [V2_635,V1_633,E2_634,P_632,E1_636,E3_637] :
( ( head_of(E3_637) != head_of(E2_634) )
| ( tail_of(E3_637) != tail_of(E1_636) )
| ~ precedes(E1_636,E2_634,P_632)
| ~ shortest_path(V1_633,V2_635,P_632) ),
inference(cnfTransformation,[status(thm)],[f_214]) ).
tff(c_1526,plain,
! [V2_649,E2_650,E1_651,V1_647,P_648] :
( ( head_of(E2_650) != head_of('#skF_12') )
| ( tail_of(E1_651) != tail_of('#skF_14') )
| ~ precedes(E1_651,E2_650,P_648)
| ~ shortest_path(V1_647,V2_649,P_648) ),
inference(superposition,[status(thm),theory(equality)],[c_1129,c_1423]) ).
tff(c_1528,plain,
! [V1_647,V2_649] :
( ( tail_of('#skF_11') != tail_of('#skF_14') )
| ~ shortest_path(V1_647,V2_649,'#skF_13') ),
inference(resolution,[status(thm)],[c_142,c_1526]) ).
tff(c_1531,plain,
! [V1_647,V2_649] : ~ shortest_path(V1_647,V2_649,'#skF_13'),
inference(demodulation,[status(thm),theory(equality)],[c_1143,c_1528]) ).
tff(c_1533,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1531,c_144]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.12 % Problem : GRA004+1 : TPTP v9.0.0. Bugfixed v3.2.0.
% 0.02/0.12 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.33 % Computer : n020.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Apr 7 20:50:04 EDT 2025
% 0.12/0.33 % CPUTime :
% 5.85/2.42 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.85/2.43
% 5.85/2.43 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------