%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : HWV089_2 : TPTP v8.1.0. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n017.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 : 600s % DateTime : Sat Jul 16 19:17:40 EDT 2022 % Result : Theorem 107.36s 104.56s % Output : Refutation 107.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : HWV089_2 : TPTP v8.1.0. Released v6.1.0. % 0.11/0.12 % Command : spasst-tptp-script %s %d % 0.13/0.33 % Computer : n017.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Thu Jun 16 21:06:41 EDT 2022 % 0.13/0.34 % CPUTime : % 0.54/0.70 % Using integer theory % 107.36/104.56 % 107.36/104.56 % 107.36/104.56 % SZS status Theorem for /tmp/SPASST_27853_n017.cluster.edu % 107.36/104.56 % 107.36/104.56 SPASS V 2.2.22 in combination with yices. % 107.36/104.56 SPASS beiseite: Proof found by SPASS. % 107.36/104.56 Problem: /tmp/SPASST_27853_n017.cluster.edu % 107.36/104.56 SPASS derived 13867 clauses, backtracked 0 clauses and kept 14321 clauses. % 107.36/104.56 SPASS backtracked 0 times (0 times due to theory inconsistency). % 107.36/104.56 SPASS allocated 38366 KBytes. % 107.36/104.56 SPASS spent 0:00:43.09 on the problem. % 107.36/104.56 0:00:00.87 for the input. % 107.36/104.56 0:00:09.05 for the FLOTTER CNF translation. % 107.36/104.56 0:00:00.00 for inferences. % 107.36/104.56 0:00:00.00 for the backtracking. % 107.36/104.56 0:00:17.92 for the reduction. % 107.36/104.56 0:00:00.25 for interacting with the SMT procedure. % 107.36/104.56 % 107.36/104.56 % 107.36/104.56 % SZS output start CNFRefutation for /tmp/SPASST_27853_n017.cluster.edu % 107.36/104.56 % 107.36/104.56 % Here is a proof with depth 1, length 22 : % 107.36/104.56 434(e)[0:Inp] || -> state_type(skc3)*. % 107.36/104.56 1002(e)[0:Inp] || v4(skc3)* -> . % 107.36/104.56 1174(e)[0:Inp] || state_type(U) -> v3679(U,1)*. % 107.36/104.56 1480(e)[0:Inp] || state_type(U) v3684(U,5)* -> . % 107.36/104.56 1483[0:Inp] || state_type(U) -> v3678(U)* v3677(U). % 107.36/104.56 1485[0:Inp] || state_type(U) -> v3674(U) v4(U)*. % 107.36/104.56 6665[0:Inp] || v3680(U) state_type(U) -> v3684(U,5)*. % 107.36/104.56 6667[0:Inp] || v3679(U,0)* state_type(U) -> v3680(U). % 107.36/104.56 6668[0:Inp] || v3678(U) state_type(U) -> v3679(U,0)*. % 107.36/104.56 6672[0:Inp] || v3679(U,1)* state_type(U) -> v3693(U). % 107.36/104.56 6673[0:Inp] || v3674(U) v3675(U)* state_type(U) -> . % 107.36/104.56 12073[0:Inp] || v3693(U)* v3677(U) state_type(U) -> v3675(U). % 107.36/104.56 14499(e)[0:MRR:6672.0,1174.1] || state_type(U) -> v3693(U)*. % 107.36/104.56 14500(e)[0:MRR:6665.2,1480.0] || state_type(U) v3680(U)* -> . % 107.36/104.56 14501(e)[0:MRR:6667.2,14500.0] || state_type(U) v3679(U,0)* -> . % 107.36/104.56 14502(e)[0:MRR:6668.2,14501.0] || state_type(U) v3678(U)* -> . % 107.36/104.56 14503(e)[0:MRR:1483.1,14502.0] || state_type(U) -> v3677(U)*. % 107.36/104.56 14557(e)[0:MRR:12073.0,12073.1,14499.1,14503.1] || state_type(U) -> v3675(U)*. % 107.36/104.56 14558(e)[0:MRR:6673.1,14557.1] || state_type(U) v3674(U)* -> . % 107.36/104.56 14559(e)[0:MRR:1485.1,14558.0] || state_type(U) -> v4(U)*. % 107.36/104.56 18465[0:Res:434.0,14559.0] || -> v4(skc3)*. % 107.36/104.56 29450[0:MRR:18465.0,1002.0] || -> . % 107.36/104.56 % 107.36/104.56 % SZS output end CNFRefutation for /tmp/SPASST_27853_n017.cluster.edu % 107.36/104.56 % 107.36/104.56 Formulae used in the proof : fof_state_type fof_pathAxiom_19 fof_addAssignment_2581 fof_writeUnaryOperator_341 fof_addZeroExtensionConstraint_7 fof_writeUnaryOperator_346 fof_writeBinaryOperatorShiftedRanges_552 fof_addAssignment_2619 fof_writeBinaryOperatorShiftedRanges_555 fof_writeBinaryOperatorShiftedRanges_551 % 113.67/108.13 % 113.67/108.13 SPASS+T ended %------------------------------------------------------------------------------