%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN036-1 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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 9 17:46:56 EDT 2024
% Result : Unsatisfiable 104.59s 104.84s
% Output : Refutation 104.59s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_67,negated_conjecture,
( ~ big_p(c11)
| big_p(X17)
| ~ big_q(X22)
| big_p(X19)
| big_q(X18)
| ~ big_q(c16)
| ~ big_p(X21)
| big_q(X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_67) ).
cnf(c2,plain,
( ~ big_p(c11)
| big_p(X23)
| ~ big_q(X25)
| big_p(X24)
| big_q(X27)
| ~ big_q(c16)
| big_q(X26) ),
inference(factor,[status(thm)],[clause_67]) ).
cnf(c3,plain,
( ~ big_p(c11)
| big_p(X37)
| ~ big_q(c16)
| big_p(X35)
| big_q(X34)
| big_q(X36) ),
inference(factor,[status(thm)],[c2]) ).
cnf(clause_65,negated_conjecture,
( ~ big_p(c11)
| big_p(X2)
| ~ big_q(X7)
| big_p(X4)
| ~ big_q(X3)
| big_q(c16)
| ~ big_p(X6)
| big_q(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_65) ).
cnf(c0,plain,
( ~ big_p(c11)
| big_p(X11)
| ~ big_q(X8)
| big_p(X12)
| ~ big_q(X10)
| big_q(c16)
| big_q(X9) ),
inference(factor,[status(thm)],[clause_65]) ).
cnf(c1,plain,
( ~ big_p(c11)
| big_p(X15)
| ~ big_q(X13)
| big_p(X14)
| big_q(c16)
| big_q(X16) ),
inference(factor,[status(thm)],[c0]) ).
cnf(clause_55,negated_conjecture,
( big_p(c3)
| ~ big_p(X348)
| big_q(c4)
| big_p(X350)
| big_q(X351)
| ~ big_q(c8)
| big_p(c9)
| big_q(X349) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_55) ).
cnf(clause_101,negated_conjecture,
( big_p(X749)
| big_p(f3(X749))
| big_q(c14)
| big_p(X750)
| big_q(f4(X751))
| big_q(X751)
| big_p(c19)
| big_q(X752) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_101) ).
cnf(c102,plain,
( big_p(X758)
| big_p(f3(X758))
| big_q(c14)
| big_q(f4(X757))
| big_q(X757)
| big_p(c19)
| big_q(X759) ),
inference(factor,[status(thm)],[clause_101]) ).
cnf(c358,plain,
( big_p(X761)
| big_p(f3(X761))
| big_q(c14)
| big_q(f4(X760))
| big_q(X760)
| big_p(c19) ),
inference(factor,[status(thm)],[c102]) ).
cnf(c575,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(f4(X762))
| big_q(X762) ),
inference(factor,[status(thm)],[c358]) ).
cnf(c724,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(f4(c14)) ),
inference(factor,[status(thm)],[c575]) ).
cnf(c887,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| ~ big_p(c11)
| big_p(X916)
| big_p(X918)
| big_q(c16)
| big_q(X917) ),
inference(resolution,[status(thm)],[c724,c1]) ).
cnf(clause_81,negated_conjecture,
( big_p(c11)
| ~ big_p(X38)
| ~ big_q(X43)
| big_p(X40)
| ~ big_q(X39)
| big_q(c16)
| ~ big_p(X42)
| big_q(X41) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_81) ).
cnf(c4,plain,
( big_p(c11)
| ~ big_p(X48)
| ~ big_q(X47)
| big_p(X46)
| ~ big_q(X45)
| big_q(c16)
| big_q(X44) ),
inference(factor,[status(thm)],[clause_81]) ).
cnf(c5,plain,
( big_p(c11)
| ~ big_p(X51)
| ~ big_q(X49)
| big_p(X50)
| big_q(c16)
| big_q(X52) ),
inference(factor,[status(thm)],[c4]) ).
cnf(c874,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_p(c11)
| ~ big_p(X905)
| big_p(X904)
| big_q(c16)
| big_q(X903) ),
inference(resolution,[status(thm)],[c724,c5]) ).
cnf(clause_5,negated_conjecture,
( big_p(X95)
| big_p(f1(X95))
| ~ big_q(X97)
| big_p(X96)
| ~ big_q(X93)
| big_q(c8)
| big_p(c9)
| big_q(X94) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_5) ).
cnf(c11,plain,
( big_p(X101)
| big_p(f1(X101))
| ~ big_q(X99)
| big_p(X100)
| big_q(c8)
| big_p(c9)
| big_q(X98) ),
inference(factor,[status(thm)],[clause_5]) ).
cnf(c885,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_p(X1331)
| big_p(f1(X1331))
| big_p(X1332)
| big_q(c8)
| big_p(c9)
| big_q(X1330) ),
inference(resolution,[status(thm)],[c724,c11]) ).
cnf(c3322,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_p(X1334)
| big_p(f1(X1334))
| big_q(c8)
| big_p(c9)
| big_q(X1333) ),
inference(factor,[status(thm)],[c885]) ).
cnf(c3677,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_p(X1335)
| big_p(f1(X1335))
| big_q(c8)
| big_p(c9) ),
inference(factor,[status(thm)],[c3322]) ).
cnf(c3957,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_p(f1(c19))
| big_q(c8)
| big_p(c9) ),
inference(factor,[status(thm)],[c3677]) ).
cnf(c4199,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_p(c9)
| big_p(c11)
| big_p(X1467)
| big_q(c16)
| big_q(X1466) ),
inference(resolution,[status(thm)],[c3957,c874]) ).
cnf(c6468,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_p(c9)
| big_p(c11)
| big_q(c16)
| big_q(X1474) ),
inference(factor,[status(thm)],[c4199]) ).
cnf(c6858,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_p(c9)
| big_p(c11)
| big_q(c16) ),
inference(factor,[status(thm)],[c6468]) ).
cnf(c7204,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_p(c11)
| big_q(c16)
| big_p(X1476)
| big_q(X1475) ),
inference(resolution,[status(thm)],[c6858,c874]) ).
cnf(c7263,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_p(c11)
| big_q(c16)
| big_q(X1484) ),
inference(factor,[status(thm)],[c7204]) ).
cnf(c7597,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_p(c11)
| big_q(c16) ),
inference(factor,[status(thm)],[c7263]) ).
cnf(c7937,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_q(c16)
| big_p(X1511)
| big_p(X1512)
| big_q(X1510) ),
inference(resolution,[status(thm)],[c7597,c887]) ).
cnf(c8786,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_q(c16)
| big_p(X1514)
| big_q(X1513) ),
inference(factor,[status(thm)],[c7937]) ).
cnf(c9161,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_q(c16)
| big_q(X1515) ),
inference(factor,[status(thm)],[c8786]) ).
cnf(c9461,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_q(c16) ),
inference(factor,[status(thm)],[c9161]) ).
cnf(c9743,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_q(c16)
| ~ big_p(c11)
| big_p(X1569)
| big_p(X1571)
| big_q(X1570) ),
inference(resolution,[status(thm)],[c9461,c1]) ).
cnf(c7881,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(c11)
| big_q(c16)
| ~ big_p(X1498)
| big_p(X1497)
| big_q(X1496) ),
inference(resolution,[status(thm)],[c7597,c5]) ).
cnf(c9804,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| ~ big_p(c11)
| big_p(X1846)
| big_p(X1845)
| big_q(X1843)
| big_q(X1844) ),
inference(resolution,[status(thm)],[c9461,c3]) ).
cnf(clause_83,negated_conjecture,
( big_p(c11)
| ~ big_p(X53)
| ~ big_q(X58)
| big_p(X55)
| big_q(X54)
| ~ big_q(c16)
| ~ big_p(X57)
| big_q(X56) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_83) ).
cnf(c6,plain,
( big_p(c11)
| ~ big_p(X67)
| ~ big_q(X65)
| big_p(X66)
| big_q(X63)
| ~ big_q(c16)
| big_q(X64) ),
inference(factor,[status(thm)],[clause_83]) ).
cnf(c8,plain,
( big_p(c11)
| ~ big_p(X70)
| ~ big_q(c16)
| big_p(X71)
| big_q(X68)
| big_q(X69) ),
inference(factor,[status(thm)],[c6]) ).
cnf(c7955,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_p(c11)
| ~ big_p(X1783)
| big_p(X1785)
| big_q(X1786)
| big_q(X1784) ),
inference(resolution,[status(thm)],[c7597,c8]) ).
cnf(c3959,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_p(c9)
| big_p(f1(c9))
| big_q(c8) ),
inference(factor,[status(thm)],[c3677]) ).
cnf(c12404,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_p(c11)
| big_p(X2027)
| big_q(X2025)
| big_q(X2026)
| big_p(c9) ),
inference(resolution,[status(thm)],[c7955,c3959]) ).
cnf(c13674,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_p(c11)
| big_q(X2028)
| big_q(X2029)
| big_p(c9) ),
inference(factor,[status(thm)],[c12404]) ).
cnf(c14145,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_p(c11)
| big_q(X2037)
| big_p(c9) ),
inference(factor,[status(thm)],[c13674]) ).
cnf(c14523,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_p(c11)
| big_p(c9) ),
inference(factor,[status(thm)],[c14145]) ).
cnf(c14946,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_p(c11)
| big_p(X2050)
| big_q(X2048)
| big_q(X2049) ),
inference(resolution,[status(thm)],[c14523,c7955]) ).
cnf(c14959,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_p(c11)
| big_q(X2051)
| big_q(X2052) ),
inference(factor,[status(thm)],[c14946]) ).
cnf(c15404,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_p(c11)
| big_q(X2053) ),
inference(factor,[status(thm)],[c14959]) ).
cnf(c15758,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_p(c11) ),
inference(factor,[status(thm)],[c15404]) ).
cnf(c16130,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_p(X2093)
| big_p(X2094)
| big_q(X2092)
| big_q(X2095) ),
inference(resolution,[status(thm)],[c15758,c9804]) ).
cnf(c16146,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_p(X2106)
| big_q(X2105)
| big_q(X2104) ),
inference(factor,[status(thm)],[c16130]) ).
cnf(c16648,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_q(X2108)
| big_q(X2107) ),
inference(factor,[status(thm)],[c16146]) ).
cnf(c17060,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8)
| big_q(X2109) ),
inference(factor,[status(thm)],[c16648]) ).
cnf(c17383,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c14)
| big_q(c8) ),
inference(factor,[status(thm)],[c17060]) ).
cnf(c17669,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(X2419)
| big_p(f1(X2419))
| big_p(X2420)
| big_p(c9)
| big_q(X2418) ),
inference(resolution,[status(thm)],[c17383,c11]) ).
cnf(c19060,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(X2421)
| big_p(f1(X2421))
| big_p(c9)
| big_q(X2422) ),
inference(factor,[status(thm)],[c17669]) ).
cnf(c19466,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(X2423)
| big_p(f1(X2423))
| big_p(c9) ),
inference(factor,[status(thm)],[c19060]) ).
cnf(c19784,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(f1(c19))
| big_p(c9) ),
inference(factor,[status(thm)],[c19466]) ).
cnf(c20109,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(c9)
| big_p(c11)
| big_q(c16)
| big_p(X2504)
| big_q(X2505) ),
inference(resolution,[status(thm)],[c19784,c7881]) ).
cnf(c20919,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(c9)
| big_p(c11)
| big_q(c16)
| big_q(X2506) ),
inference(factor,[status(thm)],[c20109]) ).
cnf(c21276,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(c9)
| big_p(c11)
| big_q(c16) ),
inference(factor,[status(thm)],[c20919]) ).
cnf(c21644,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(c11)
| big_q(c16)
| big_p(X2514)
| big_q(X2515) ),
inference(resolution,[status(thm)],[c21276,c7881]) ).
cnf(c21731,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(c11)
| big_q(c16)
| big_q(X2516) ),
inference(factor,[status(thm)],[c21644]) ).
cnf(c22065,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(c11)
| big_q(c16) ),
inference(factor,[status(thm)],[c21731]) ).
cnf(c22410,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_q(c16)
| big_p(X2539)
| big_p(X2540)
| big_q(X2538) ),
inference(resolution,[status(thm)],[c22065,c9743]) ).
cnf(c22611,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_q(c16)
| big_p(X2542)
| big_q(X2541) ),
inference(factor,[status(thm)],[c22410]) ).
cnf(c22997,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_q(c16)
| big_q(X2543) ),
inference(factor,[status(thm)],[c22611]) ).
cnf(c23298,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_q(c16) ),
inference(factor,[status(thm)],[c22997]) ).
cnf(c23622,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| ~ big_p(c11)
| big_p(X2763)
| big_p(X2762)
| big_q(X2760)
| big_q(X2761) ),
inference(resolution,[status(thm)],[c23298,c3]) ).
cnf(c22428,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(c11)
| ~ big_p(X2730)
| big_p(X2732)
| big_q(X2733)
| big_q(X2731) ),
inference(resolution,[status(thm)],[c22065,c8]) ).
cnf(c19785,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(f1(f3(c19)))
| big_p(c9) ),
inference(factor,[status(thm)],[c19466]) ).
cnf(c26240,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(c11)
| big_p(X2885)
| big_q(X2883)
| big_q(X2884)
| big_p(c9) ),
inference(resolution,[status(thm)],[c22428,c19785]) ).
cnf(c26663,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(c11)
| big_q(X2887)
| big_q(X2886)
| big_p(c9) ),
inference(factor,[status(thm)],[c26240]) ).
cnf(c27079,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(c11)
| big_q(X2888)
| big_p(c9) ),
inference(factor,[status(thm)],[c26663]) ).
cnf(c27411,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(c11)
| big_p(c9) ),
inference(factor,[status(thm)],[c27079]) ).
cnf(c27748,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(c11)
| big_p(X2899)
| big_q(X2897)
| big_q(X2898) ),
inference(resolution,[status(thm)],[c27411,c22428]) ).
cnf(c27775,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(c11)
| big_q(X2901)
| big_q(X2900) ),
inference(factor,[status(thm)],[c27748]) ).
cnf(c28173,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(c11)
| big_q(X2902) ),
inference(factor,[status(thm)],[c27775]) ).
cnf(c28489,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(c11) ),
inference(factor,[status(thm)],[c28173]) ).
cnf(c28810,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(X2928)
| big_p(X2930)
| big_q(X2929)
| big_q(X2927) ),
inference(resolution,[status(thm)],[c28489,c23622]) ).
cnf(c28819,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_p(X2938)
| big_q(X2937)
| big_q(X2939) ),
inference(factor,[status(thm)],[c28810]) ).
cnf(c29304,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_q(X2940)
| big_q(X2941) ),
inference(factor,[status(thm)],[c28819]) ).
cnf(c29682,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8)
| big_q(X2942) ),
inference(factor,[status(thm)],[c29304]) ).
cnf(c29980,plain,
( big_p(c19)
| big_p(f3(c19))
| big_q(c8) ),
inference(factor,[status(thm)],[c29682]) ).
cnf(clause_53,negated_conjecture,
( big_p(c3)
| ~ big_p(X328)
| big_q(c4)
| big_p(X330)
| ~ big_q(X331)
| big_q(c8)
| big_p(c9)
| big_q(X329) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_53) ).
cnf(clause_49,negated_conjecture,
( big_p(c3)
| ~ big_p(X314)
| big_q(c4)
| big_p(X316)
| big_q(f2(X315))
| big_q(X315)
| ~ big_p(X318)
| big_q(X317) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_49) ).
cnf(c39,plain,
( big_p(c3)
| ~ big_p(X320)
| big_q(c4)
| big_p(X319)
| big_q(f2(X322))
| big_q(X322)
| big_q(X321) ),
inference(factor,[status(thm)],[clause_49]) ).
cnf(c30202,plain,
( big_p(c19)
| big_q(c8)
| big_p(c3)
| big_q(c4)
| big_p(X3327)
| big_q(f2(X3328))
| big_q(X3328)
| big_q(X3326) ),
inference(resolution,[status(thm)],[c29980,c39]) ).
cnf(c34466,plain,
( big_p(c19)
| big_q(c8)
| big_p(c3)
| big_q(c4)
| big_q(f2(X3330))
| big_q(X3330)
| big_q(X3329) ),
inference(factor,[status(thm)],[c30202]) ).
cnf(c34919,plain,
( big_p(c19)
| big_q(c8)
| big_p(c3)
| big_q(c4)
| big_q(f2(X3331))
| big_q(X3331) ),
inference(factor,[status(thm)],[c34466]) ).
cnf(c35282,plain,
( big_p(c19)
| big_q(c8)
| big_p(c3)
| big_q(c4)
| big_q(f2(c8)) ),
inference(factor,[status(thm)],[c34919]) ).
cnf(c35641,plain,
( big_p(c19)
| big_q(c8)
| big_p(c3)
| big_q(c4)
| ~ big_p(X3389)
| big_p(X3390)
| big_p(c9)
| big_q(X3388) ),
inference(resolution,[status(thm)],[c35282,clause_53]) ).
cnf(c36667,plain,
( big_p(c19)
| big_q(c8)
| big_p(c3)
| big_q(c4)
| big_p(X3399)
| big_p(c9)
| big_q(X3398) ),
inference(resolution,[status(thm)],[c35641,c29980]) ).
cnf(c36809,plain,
( big_p(c19)
| big_q(c8)
| big_p(c3)
| big_q(c4)
| big_p(c9)
| big_q(X3400) ),
inference(factor,[status(thm)],[c36667]) ).
cnf(c37133,plain,
( big_p(c19)
| big_q(c8)
| big_p(c3)
| big_q(c4)
| big_p(c9) ),
inference(factor,[status(thm)],[c36809]) ).
cnf(c37383,plain,
( big_q(c8)
| big_p(c3)
| big_q(c4)
| big_p(c9)
| big_p(X3554)
| big_q(f2(X3555))
| big_q(X3555)
| big_q(X3553) ),
inference(resolution,[status(thm)],[c37133,c39]) ).
cnf(c37978,plain,
( big_q(c8)
| big_p(c3)
| big_q(c4)
| big_p(c9)
| big_p(X3556)
| big_q(f2(X3557))
| big_q(X3557) ),
inference(factor,[status(thm)],[c37383]) ).
cnf(c38450,plain,
( big_q(c8)
| big_p(c3)
| big_q(c4)
| big_p(c9)
| big_q(f2(X3558))
| big_q(X3558) ),
inference(factor,[status(thm)],[c37978]) ).
cnf(c38802,plain,
( big_q(c8)
| big_p(c3)
| big_q(c4)
| big_p(c9)
| big_q(f2(c8)) ),
inference(factor,[status(thm)],[c38450]) ).
cnf(c39216,plain,
( big_q(c8)
| big_p(c3)
| big_q(c4)
| big_p(c9)
| ~ big_p(X3578)
| big_p(X3579)
| big_q(X3577) ),
inference(resolution,[status(thm)],[c38802,clause_53]) ).
cnf(c39494,plain,
( big_q(c8)
| big_p(c3)
| big_q(c4)
| big_p(c9)
| big_p(X3581)
| big_q(X3580) ),
inference(resolution,[status(thm)],[c39216,c37133]) ).
cnf(c39555,plain,
( big_q(c8)
| big_p(c3)
| big_q(c4)
| big_p(c9)
| big_p(X3589) ),
inference(factor,[status(thm)],[c39494]) ).
cnf(c39977,plain,
( big_q(c8)
| big_p(c3)
| big_q(c4)
| big_p(c9) ),
inference(factor,[status(thm)],[c39555]) ).
cnf(c40195,plain,
( big_p(c3)
| big_q(c4)
| big_p(c9)
| ~ big_p(X3620)
| big_p(X3619)
| big_q(X3618)
| big_q(X3621) ),
inference(resolution,[status(thm)],[c39977,clause_55]) ).
cnf(clause_7,negated_conjecture,
( big_p(X113)
| big_p(f1(X113))
| ~ big_q(X115)
| big_p(X114)
| big_q(X111)
| ~ big_q(c8)
| big_p(c9)
| big_q(X112) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_7) ).
cnf(c14,plain,
( big_p(X122)
| big_p(f1(X122))
| ~ big_q(c8)
| big_p(X121)
| big_q(X123)
| big_p(c9)
| big_q(X120) ),
inference(factor,[status(thm)],[clause_7]) ).
cnf(c40186,plain,
( big_p(c3)
| big_q(c4)
| big_p(c9)
| big_p(X4168)
| big_p(f1(X4168))
| big_p(X4169)
| big_q(X4170)
| big_q(X4171) ),
inference(resolution,[status(thm)],[c39977,c14]) ).
cnf(c46354,plain,
( big_p(c3)
| big_q(c4)
| big_p(c9)
| big_p(X4173)
| big_p(f1(X4173))
| big_q(X4172)
| big_q(X4174) ),
inference(factor,[status(thm)],[c40186]) ).
cnf(c46934,plain,
( big_p(c3)
| big_q(c4)
| big_p(c9)
| big_p(X4180)
| big_p(f1(X4180))
| big_q(X4181) ),
inference(factor,[status(thm)],[c46354]) ).
cnf(c47410,plain,
( big_p(c3)
| big_q(c4)
| big_p(c9)
| big_p(X4182)
| big_p(f1(X4182)) ),
inference(factor,[status(thm)],[c46934]) ).
cnf(c47755,plain,
( big_p(c3)
| big_q(c4)
| big_p(c9)
| big_p(f1(c3)) ),
inference(factor,[status(thm)],[c47410]) ).
cnf(c48053,plain,
( big_p(c3)
| big_q(c4)
| big_p(c9)
| big_p(X4193)
| big_q(X4191)
| big_q(X4192) ),
inference(resolution,[status(thm)],[c47755,c40195]) ).
cnf(c48202,plain,
( big_p(c3)
| big_q(c4)
| big_p(c9)
| big_q(X4194)
| big_q(X4195) ),
inference(factor,[status(thm)],[c48053]) ).
cnf(c48638,plain,
( big_p(c3)
| big_q(c4)
| big_p(c9)
| big_q(X4196) ),
inference(factor,[status(thm)],[c48202]) ).
cnf(c48973,plain,
( big_p(c3)
| big_q(c4)
| big_p(c9) ),
inference(factor,[status(thm)],[c48638]) ).
cnf(c49252,plain,
( big_p(c3)
| big_q(c4)
| big_p(X4239)
| big_q(f2(X4240))
| big_q(X4240)
| big_q(X4238) ),
inference(resolution,[status(thm)],[c48973,c39]) ).
cnf(c49253,plain,
( big_p(c3)
| big_q(c4)
| big_q(f2(X4242))
| big_q(X4242)
| big_q(X4241) ),
inference(factor,[status(thm)],[c49252]) ).
cnf(c49704,plain,
( big_p(c3)
| big_q(c4)
| big_q(f2(X4243))
| big_q(X4243) ),
inference(factor,[status(thm)],[c49253]) ).
cnf(c50055,plain,
( big_p(c3)
| big_q(c4)
| big_q(f2(c4)) ),
inference(factor,[status(thm)],[c49704]) ).
cnf(c50337,plain,
( big_p(c3)
| big_q(c4)
| big_p(c11)
| ~ big_p(X4442)
| big_p(X4441)
| big_q(c16)
| big_q(X4440) ),
inference(resolution,[status(thm)],[c50055,c5]) ).
cnf(c52247,plain,
( big_p(c3)
| big_q(c4)
| big_p(c11)
| big_p(X4448)
| big_q(c16)
| big_q(X4447) ),
inference(resolution,[status(thm)],[c50337,c48973]) ).
cnf(c52258,plain,
( big_p(c3)
| big_q(c4)
| big_p(c11)
| big_q(c16)
| big_q(X4449) ),
inference(factor,[status(thm)],[c52247]) ).
cnf(c52612,plain,
( big_p(c3)
| big_q(c4)
| big_p(c11)
| big_q(c16) ),
inference(factor,[status(thm)],[c52258]) ).
cnf(c52954,plain,
( big_p(c3)
| big_q(c4)
| big_p(c11)
| ~ big_p(X4478)
| big_p(X4480)
| big_q(X4481)
| big_q(X4479) ),
inference(resolution,[status(thm)],[c52612,c8]) ).
cnf(c53164,plain,
( big_p(c3)
| big_q(c4)
| big_p(c11)
| big_p(X4484)
| big_q(X4482)
| big_q(X4483) ),
inference(resolution,[status(thm)],[c52954,c48973]) ).
cnf(c53175,plain,
( big_p(c3)
| big_q(c4)
| big_p(c11)
| big_q(X4492)
| big_q(X4493) ),
inference(factor,[status(thm)],[c53164]) ).
cnf(c53617,plain,
( big_p(c3)
| big_q(c4)
| big_p(c11)
| big_q(X4494) ),
inference(factor,[status(thm)],[c53175]) ).
cnf(c53955,plain,
( big_p(c3)
| big_q(c4)
| big_p(c11) ),
inference(factor,[status(thm)],[c53617]) ).
cnf(c50367,plain,
( big_p(c3)
| big_q(c4)
| ~ big_p(c11)
| big_p(X4549)
| big_p(X4551)
| big_q(c16)
| big_q(X4550) ),
inference(resolution,[status(thm)],[c50055,c1]) ).
cnf(c54301,plain,
( big_p(c3)
| big_q(c4)
| big_p(X4554)
| big_p(X4552)
| big_q(c16)
| big_q(X4553) ),
inference(resolution,[status(thm)],[c50367,c53955]) ).
cnf(c54315,plain,
( big_p(c3)
| big_q(c4)
| big_p(X4556)
| big_q(c16)
| big_q(X4555) ),
inference(factor,[status(thm)],[c54301]) ).
cnf(c54743,plain,
( big_p(c3)
| big_q(c4)
| big_q(c16)
| big_q(X4557) ),
inference(factor,[status(thm)],[c54315]) ).
cnf(c55066,plain,
( big_p(c3)
| big_q(c4)
| big_q(c16) ),
inference(factor,[status(thm)],[c54743]) ).
cnf(c55372,plain,
( big_p(c3)
| big_q(c4)
| ~ big_p(c11)
| big_p(X4634)
| big_p(X4633)
| big_q(X4631)
| big_q(X4632) ),
inference(resolution,[status(thm)],[c55066,c3]) ).
cnf(c55461,plain,
( big_p(c3)
| big_q(c4)
| big_p(X4636)
| big_p(X4638)
| big_q(X4637)
| big_q(X4635) ),
inference(resolution,[status(thm)],[c55372,c53955]) ).
cnf(c55475,plain,
( big_p(c3)
| big_q(c4)
| big_p(X4639)
| big_q(X4640)
| big_q(X4641) ),
inference(factor,[status(thm)],[c55461]) ).
cnf(c55982,plain,
( big_p(c3)
| big_q(c4)
| big_q(X4642)
| big_q(X4643) ),
inference(factor,[status(thm)],[c55475]) ).
cnf(c56386,plain,
( big_p(c3)
| big_q(c4)
| big_q(X4644) ),
inference(factor,[status(thm)],[c55982]) ).
cnf(c56686,plain,
( big_p(c3)
| big_q(c4) ),
inference(factor,[status(thm)],[c56386]) ).
cnf(clause_33,negated_conjecture,
( ~ big_p(c3)
| big_p(X196)
| big_q(c4)
| big_p(X198)
| big_q(f2(X197))
| big_q(X197)
| ~ big_p(X200)
| big_q(X199) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_33) ).
cnf(c21,plain,
( ~ big_p(c3)
| big_p(X204)
| big_q(c4)
| big_p(X203)
| big_q(f2(X202))
| big_q(X202)
| big_q(X201) ),
inference(factor,[status(thm)],[clause_33]) ).
cnf(c56875,plain,
( big_q(c4)
| big_p(X4705)
| big_p(X4707)
| big_q(f2(X4704))
| big_q(X4704)
| big_q(X4706) ),
inference(resolution,[status(thm)],[c56686,c21]) ).
cnf(c56940,plain,
( big_q(c4)
| big_p(X4709)
| big_p(X4710)
| big_q(f2(X4708))
| big_q(X4708) ),
inference(factor,[status(thm)],[c56875]) ).
cnf(c57431,plain,
( big_q(c4)
| big_p(X4712)
| big_q(f2(X4711))
| big_q(X4711) ),
inference(factor,[status(thm)],[c56940]) ).
cnf(c57799,plain,
( big_q(c4)
| big_p(X4719)
| big_q(f2(c4)) ),
inference(factor,[status(thm)],[c57431]) ).
cnf(c58199,plain,
( big_q(c4)
| big_p(X4832)
| big_p(c11)
| ~ big_p(X4831)
| big_p(X4830)
| big_q(c16)
| big_q(X4829) ),
inference(resolution,[status(thm)],[c57799,c5]) ).
cnf(c58311,plain,
( big_q(c4)
| big_p(X4835)
| big_p(c11)
| big_p(X4833)
| big_q(c16)
| big_q(X4834) ),
inference(resolution,[status(thm)],[c58199,c56686]) ).
cnf(c58315,plain,
( big_q(c4)
| big_p(X4837)
| big_p(c11)
| big_p(X4836)
| big_q(c16) ),
inference(factor,[status(thm)],[c58311]) ).
cnf(c58714,plain,
( big_q(c4)
| big_p(c11)
| big_p(X4838)
| big_q(c16) ),
inference(factor,[status(thm)],[c58315]) ).
cnf(c58994,plain,
( big_q(c4)
| big_p(c11)
| big_q(c16) ),
inference(factor,[status(thm)],[c58714]) ).
cnf(c59239,plain,
( big_q(c4)
| big_p(c11)
| ~ big_p(X4878)
| big_p(X4880)
| big_q(X4881)
| big_q(X4879) ),
inference(resolution,[status(thm)],[c58994,c8]) ).
cnf(c59436,plain,
( big_q(c4)
| big_p(c11)
| big_p(X4883)
| big_q(X4882)
| big_q(X4884) ),
inference(resolution,[status(thm)],[c59239,c56686]) ).
cnf(c59440,plain,
( big_q(c4)
| big_p(c11)
| big_p(X4885)
| big_q(X4886) ),
inference(factor,[status(thm)],[c59436]) ).
cnf(c59815,plain,
( big_q(c4)
| big_p(c11)
| big_p(X4887) ),
inference(factor,[status(thm)],[c59440]) ).
cnf(c60072,plain,
( big_q(c4)
| big_p(c11) ),
inference(factor,[status(thm)],[c59815]) ).
cnf(c58228,plain,
( big_q(c4)
| big_p(X5352)
| ~ big_p(c11)
| big_p(X5349)
| big_p(X5351)
| big_q(c16)
| big_q(X5350) ),
inference(resolution,[status(thm)],[c57799,c1]) ).
cnf(c65476,plain,
( big_q(c4)
| big_p(X5356)
| big_p(X5353)
| big_p(X5355)
| big_q(c16)
| big_q(X5354) ),
inference(resolution,[status(thm)],[c58228,c60072]) ).
cnf(c65477,plain,
( big_q(c4)
| big_p(X5359)
| big_p(X5357)
| big_p(X5358)
| big_q(c16) ),
inference(factor,[status(thm)],[c65476]) ).
cnf(c65931,plain,
( big_q(c4)
| big_p(X5361)
| big_p(X5360)
| big_q(c16) ),
inference(factor,[status(thm)],[c65477]) ).
cnf(c66267,plain,
( big_q(c4)
| big_p(X5368)
| big_q(c16) ),
inference(factor,[status(thm)],[c65931]) ).
cnf(c66552,plain,
( big_p(X5393)
| big_q(c16)
| ~ big_p(c11)
| big_p(X5394)
| big_p(X5396)
| big_q(X5395) ),
inference(resolution,[status(thm)],[c66267,c1]) ).
cnf(c59183,plain,
( big_p(c11)
| big_q(c16)
| ~ big_p(X4849)
| big_p(X4848)
| big_q(X4847) ),
inference(resolution,[status(thm)],[c58994,c5]) ).
cnf(c576,plain,
( big_p(X763)
| big_p(f3(X763))
| big_q(c14)
| big_q(f4(c14))
| big_p(c19) ),
inference(factor,[status(thm)],[c358]) ).
cnf(c949,plain,
( big_p(X985)
| big_p(f3(X985))
| big_q(c14)
| big_p(c19)
| big_p(c11)
| ~ big_p(X986)
| big_p(X987)
| big_q(c16)
| big_q(X984) ),
inference(resolution,[status(thm)],[c576,c5]) ).
cnf(c7857,plain,
( big_p(c19)
| big_q(c14)
| big_q(c8)
| big_p(c11)
| big_q(c16)
| big_p(X1680)
| big_p(f3(X1680))
| big_p(X1681)
| big_q(X1679) ),
inference(resolution,[status(thm)],[c7597,c949]) ).
cnf(c10881,plain,
( big_p(c19)
| big_q(c14)
| big_q(c8)
| big_p(c11)
| big_q(c16)
| big_p(X1683)
| big_p(f3(X1683))
| big_q(X1682) ),
inference(factor,[status(thm)],[c7857]) ).
cnf(c11288,plain,
( big_p(c19)
| big_q(c14)
| big_q(c8)
| big_p(c11)
| big_q(c16)
| big_p(X1684)
| big_p(f3(X1684)) ),
inference(factor,[status(thm)],[c10881]) ).
cnf(c11616,plain,
( big_p(c19)
| big_q(c14)
| big_q(c8)
| big_p(c11)
| big_q(c16)
| big_p(f3(c11)) ),
inference(factor,[status(thm)],[c11288]) ).
cnf(c11869,plain,
( big_p(c19)
| big_q(c8)
| big_p(c11)
| big_q(c16)
| big_p(f3(c11))
| ~ big_p(X1722)
| big_p(X1721)
| big_q(X1720) ),
inference(resolution,[status(thm)],[c11616,c5]) ).
cnf(c22348,plain,
( big_p(c19)
| big_q(c8)
| big_p(c11)
| big_q(c16)
| big_p(f3(c11))
| big_p(X2587)
| big_q(X2586) ),
inference(resolution,[status(thm)],[c22065,c11869]) ).
cnf(c23646,plain,
( big_p(c19)
| big_q(c8)
| big_p(c11)
| big_q(c16)
| big_p(f3(c11))
| big_q(X2588) ),
inference(factor,[status(thm)],[c22348]) ).
cnf(c23966,plain,
( big_p(c19)
| big_q(c8)
| big_p(c11)
| big_q(c16)
| big_p(f3(c11)) ),
inference(factor,[status(thm)],[c23646]) ).
cnf(c24283,plain,
( big_p(c19)
| big_q(c8)
| big_p(c11)
| big_p(f3(c11))
| ~ big_p(X2774)
| big_p(X2776)
| big_q(X2777)
| big_q(X2775) ),
inference(resolution,[status(thm)],[c23966,c8]) ).
cnf(c28751,plain,
( big_p(c19)
| big_q(c8)
| big_p(c11)
| big_p(f3(c11))
| big_p(X3006)
| big_q(X3007)
| big_q(X3005) ),
inference(resolution,[status(thm)],[c28489,c24283]) ).
cnf(c31064,plain,
( big_p(c19)
| big_q(c8)
| big_p(c11)
| big_p(f3(c11))
| big_q(X3008)
| big_q(X3009) ),
inference(factor,[status(thm)],[c28751]) ).
cnf(c31463,plain,
( big_p(c19)
| big_q(c8)
| big_p(c11)
| big_p(f3(c11))
| big_q(X3010) ),
inference(factor,[status(thm)],[c31064]) ).
cnf(c31782,plain,
( big_p(c19)
| big_q(c8)
| big_p(c11)
| big_p(f3(c11)) ),
inference(factor,[status(thm)],[c31463]) ).
cnf(c59309,plain,
( big_p(c11)
| big_q(c16)
| big_p(X4957)
| big_q(X4956)
| big_p(c19)
| big_q(c8) ),
inference(resolution,[status(thm)],[c59183,c31782]) ).
cnf(c60321,plain,
( big_p(c11)
| big_q(c16)
| big_q(X4965)
| big_p(c19)
| big_q(c8) ),
inference(factor,[status(thm)],[c59309]) ).
cnf(c60642,plain,
( big_p(c11)
| big_q(c16)
| big_p(c19)
| big_q(c8) ),
inference(factor,[status(thm)],[c60321]) ).
cnf(c60932,plain,
( big_p(c11)
| big_q(c16)
| big_q(c8)
| big_p(X4967)
| big_q(X4966) ),
inference(resolution,[status(thm)],[c60642,c59183]) ).
cnf(c60983,plain,
( big_p(c11)
| big_q(c16)
| big_q(c8)
| big_q(X4968) ),
inference(factor,[status(thm)],[c60932]) ).
cnf(c61287,plain,
( big_p(c11)
| big_q(c16)
| big_q(c8) ),
inference(factor,[status(thm)],[c60983]) ).
cnf(c61531,plain,
( big_p(c11)
| big_q(c8)
| ~ big_p(X4988)
| big_p(X4990)
| big_q(X4991)
| big_q(X4989) ),
inference(resolution,[status(thm)],[c61287,c8]) ).
cnf(c61635,plain,
( big_p(c11)
| big_q(c8)
| big_p(X5052)
| big_q(X5051)
| big_q(X5050)
| big_p(c19) ),
inference(resolution,[status(thm)],[c61531,c31782]) ).
cnf(c62715,plain,
( big_p(c11)
| big_q(c8)
| big_q(X5054)
| big_q(X5053)
| big_p(c19) ),
inference(factor,[status(thm)],[c61635]) ).
cnf(c63120,plain,
( big_p(c11)
| big_q(c8)
| big_q(X5055)
| big_p(c19) ),
inference(factor,[status(thm)],[c62715]) ).
cnf(c63432,plain,
( big_p(c11)
| big_q(c8)
| big_p(c19) ),
inference(factor,[status(thm)],[c63120]) ).
cnf(c63692,plain,
( big_p(c11)
| big_q(c8)
| big_p(X5067)
| big_q(X5066)
| big_q(X5065) ),
inference(resolution,[status(thm)],[c63432,c61531]) ).
cnf(c63706,plain,
( big_p(c11)
| big_q(c8)
| big_q(X5068)
| big_q(X5069) ),
inference(factor,[status(thm)],[c63692]) ).
cnf(c64091,plain,
( big_p(c11)
| big_q(c8)
| big_q(X5076) ),
inference(factor,[status(thm)],[c63706]) ).
cnf(c64456,plain,
( big_p(c11)
| big_q(c8) ),
inference(factor,[status(thm)],[c64091]) ).
cnf(c66689,plain,
( big_p(X5408)
| big_q(c16)
| big_p(X5405)
| big_p(X5407)
| big_q(X5406)
| big_q(c8) ),
inference(resolution,[status(thm)],[c66552,c64456]) ).
cnf(c66737,plain,
( big_p(X5409)
| big_q(c16)
| big_p(X5410)
| big_q(X5411)
| big_q(c8) ),
inference(factor,[status(thm)],[c66689]) ).
cnf(c67183,plain,
( big_p(X5412)
| big_q(c16)
| big_q(X5413)
| big_q(c8) ),
inference(factor,[status(thm)],[c66737]) ).
cnf(c67540,plain,
( big_p(X5414)
| big_q(c16)
| big_q(c8) ),
inference(factor,[status(thm)],[c67183]) ).
cnf(c67922,plain,
( big_p(X5719)
| big_q(c8)
| ~ big_p(c11)
| big_p(X5723)
| big_p(X5721)
| big_q(X5722)
| big_q(X5720) ),
inference(resolution,[status(thm)],[c67540,c3]) ).
cnf(c71103,plain,
( big_p(X5725)
| big_q(c8)
| big_p(X5728)
| big_p(X5727)
| big_q(X5726)
| big_q(X5724) ),
inference(resolution,[status(thm)],[c67922,c64456]) ).
cnf(c71124,plain,
( big_p(X5738)
| big_q(c8)
| big_p(X5737)
| big_q(X5735)
| big_q(X5736) ),
inference(factor,[status(thm)],[c71103]) ).
cnf(c71589,plain,
( big_p(X5740)
| big_q(c8)
| big_q(X5741)
| big_q(X5739) ),
inference(factor,[status(thm)],[c71124]) ).
cnf(c71973,plain,
( big_p(X5742)
| big_q(c8)
| big_q(X5743) ),
inference(factor,[status(thm)],[c71589]) ).
cnf(c72278,plain,
( big_p(X5744)
| big_q(c8) ),
inference(factor,[status(thm)],[c71973]) ).
cnf(c72551,plain,
( big_p(X6537)
| big_p(X6533)
| big_p(f1(X6533))
| big_p(X6534)
| big_q(X6535)
| big_p(c9)
| big_q(X6536) ),
inference(resolution,[status(thm)],[c72278,c14]) ).
cnf(c73090,plain,
( big_p(X6546)
| big_p(f1(X6546))
| big_p(X6545)
| big_q(X6543)
| big_p(c9)
| big_q(X6544) ),
inference(factor,[status(thm)],[c72551]) ).
cnf(c73505,plain,
( big_p(X6547)
| big_p(f1(X6547))
| big_q(X6549)
| big_p(c9)
| big_q(X6548) ),
inference(factor,[status(thm)],[c73090]) ).
cnf(c73855,plain,
( big_p(X6551)
| big_p(f1(X6551))
| big_q(X6550)
| big_p(c9) ),
inference(factor,[status(thm)],[c73505]) ).
cnf(c74138,plain,
( big_p(c9)
| big_p(f1(c9))
| big_q(X6552) ),
inference(factor,[status(thm)],[c73855]) ).
cnf(c74341,plain,
( big_p(c9)
| big_q(X6611)
| big_p(c11)
| big_q(c16)
| big_p(X6612)
| big_q(X6610) ),
inference(resolution,[status(thm)],[c74138,c59183]) ).
cnf(c74473,plain,
( big_p(c9)
| big_q(X6613)
| big_p(c11)
| big_q(c16)
| big_q(X6614) ),
inference(factor,[status(thm)],[c74341]) ).
cnf(c74785,plain,
( big_p(c9)
| big_q(c16)
| big_p(c11)
| big_q(X6615) ),
inference(factor,[status(thm)],[c74473]) ).
cnf(c75035,plain,
( big_p(c9)
| big_q(c16)
| big_p(c11) ),
inference(factor,[status(thm)],[c74785]) ).
cnf(c75190,plain,
( big_q(c16)
| big_p(c11)
| big_p(X6622)
| big_q(X6621) ),
inference(resolution,[status(thm)],[c75035,c59183]) ).
cnf(c75251,plain,
( big_q(c16)
| big_p(c11)
| big_p(X6623) ),
inference(factor,[status(thm)],[c75190]) ).
cnf(c75452,plain,
( big_q(c16)
| big_p(c11) ),
inference(factor,[status(thm)],[c75251]) ).
cnf(c75591,plain,
( big_q(c16)
| big_p(X6640)
| big_p(X6637)
| big_p(X6639)
| big_q(X6638) ),
inference(resolution,[status(thm)],[c75452,c66552]) ).
cnf(c75687,plain,
( big_q(c16)
| big_p(X6641)
| big_p(X6642)
| big_p(X6643) ),
inference(factor,[status(thm)],[c75591]) ).
cnf(c75951,plain,
( big_q(c16)
| big_p(X6649)
| big_p(X6650) ),
inference(factor,[status(thm)],[c75687]) ).
cnf(c76131,plain,
( big_q(c16)
| big_p(X6651) ),
inference(factor,[status(thm)],[c75951]) ).
cnf(c76269,plain,
( big_p(X6770)
| ~ big_p(c11)
| big_p(X6769)
| big_p(X6767)
| big_q(X6768)
| big_q(X6766) ),
inference(resolution,[status(thm)],[c76131,c3]) ).
cnf(c75575,plain,
( big_p(c11)
| ~ big_p(X6633)
| big_p(X6635)
| big_q(X6636)
| big_q(X6634) ),
inference(resolution,[status(thm)],[c75452,c8]) ).
cnf(c75658,plain,
( big_p(c11)
| big_p(X6829)
| big_q(X6828)
| big_q(X6827)
| big_p(c9)
| big_q(X6826) ),
inference(resolution,[status(thm)],[c75575,c74138]) ).
cnf(c76359,plain,
( big_p(c11)
| big_q(X6832)
| big_q(X6831)
| big_p(c9)
| big_q(X6830) ),
inference(factor,[status(thm)],[c75658]) ).
cnf(c76632,plain,
( big_p(c11)
| big_q(X6834)
| big_p(c9)
| big_q(X6833) ),
inference(factor,[status(thm)],[c76359]) ).
cnf(c76861,plain,
( big_p(c11)
| big_q(X6839)
| big_p(c9) ),
inference(factor,[status(thm)],[c76632]) ).
cnf(c77105,plain,
( big_p(c11)
| big_q(X6844)
| big_p(X6847)
| big_q(X6846)
| big_q(X6845) ),
inference(resolution,[status(thm)],[c76861,c75575]) ).
cnf(c77107,plain,
( big_p(c11)
| big_q(X6850)
| big_q(X6849)
| big_q(X6848) ),
inference(factor,[status(thm)],[c77105]) ).
cnf(c77370,plain,
( big_p(c11)
| big_q(X6858)
| big_q(X6857) ),
inference(factor,[status(thm)],[c77107]) ).
cnf(c77584,plain,
( big_p(c11)
| big_q(X6859) ),
inference(factor,[status(thm)],[c77370]) ).
cnf(c77732,plain,
( big_q(X6904)
| big_p(X6903)
| big_p(X6907)
| big_p(X6906)
| big_q(X6902)
| big_q(X6905) ),
inference(resolution,[status(thm)],[c77584,c76269]) ).
cnf(c77833,plain,
( big_q(X6912)
| big_p(X6910)
| big_p(X6909)
| big_p(X6911)
| big_q(X6908) ),
inference(factor,[status(thm)],[c77732]) ).
cnf(c78058,plain,
( big_q(X6922)
| big_p(X6919)
| big_p(X6921)
| big_p(X6920) ),
inference(factor,[status(thm)],[c77833]) ).
cnf(c78225,plain,
( big_q(X6925)
| big_p(X6924)
| big_p(X6923) ),
inference(factor,[status(thm)],[c78058]) ).
cnf(c78341,plain,
( big_q(X6926)
| big_p(X6927) ),
inference(factor,[status(thm)],[c78225]) ).
cnf(clause_72,negated_conjecture,
( ~ big_p(c11)
| big_p(X501)
| ~ big_q(X504)
| big_p(X503)
| ~ big_q(f4(X502))
| ~ big_q(X502)
| ~ big_p(X505)
| ~ big_q(c20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_72) ).
cnf(c70,plain,
( ~ big_p(c11)
| big_p(X507)
| ~ big_q(f4(X509))
| big_p(X506)
| ~ big_q(X509)
| ~ big_p(X508)
| ~ big_q(c20) ),
inference(factor,[status(thm)],[clause_72]) ).
cnf(c78406,plain,
( big_p(X7661)
| ~ big_p(c11)
| big_p(X7658)
| big_p(X7662)
| ~ big_q(X7660)
| ~ big_p(X7659)
| ~ big_q(c20) ),
inference(resolution,[status(thm)],[c78341,c70]) ).
cnf(c78425,plain,
( big_p(X7666)
| ~ big_p(c11)
| big_p(X7665)
| big_p(X7664)
| ~ big_q(c20)
| ~ big_p(X7663) ),
inference(factor,[status(thm)],[c78406]) ).
cnf(c78427,plain,
( big_p(X7674)
| ~ big_p(c11)
| big_p(X7672)
| big_p(X7673)
| ~ big_q(c20) ),
inference(factor,[status(thm)],[c78425]) ).
cnf(c78429,plain,
( big_p(X7675)
| ~ big_p(c11)
| big_p(X7676)
| big_p(X7677)
| big_p(X7678) ),
inference(resolution,[status(thm)],[c78427,c78341]) ).
cnf(clause_88,negated_conjecture,
( big_p(c11)
| ~ big_p(X594)
| ~ big_q(X597)
| big_p(X596)
| ~ big_q(f4(X595))
| ~ big_q(X595)
| ~ big_p(X598)
| ~ big_q(c20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_88) ).
cnf(c84,plain,
( big_p(c11)
| ~ big_p(X602)
| ~ big_q(f4(X601))
| big_p(X599)
| ~ big_q(X601)
| ~ big_p(X600)
| ~ big_q(c20) ),
inference(factor,[status(thm)],[clause_88]) ).
cnf(c77786,plain,
( big_p(c11)
| ~ big_p(X7109)
| big_p(X7110)
| ~ big_q(X7107)
| ~ big_p(X7108)
| ~ big_q(c20) ),
inference(resolution,[status(thm)],[c77584,c84]) ).
cnf(c78419,plain,
( big_p(c11)
| ~ big_p(X7111)
| big_p(X7113)
| ~ big_q(c20)
| ~ big_p(X7112) ),
inference(factor,[status(thm)],[c77786]) ).
cnf(c78421,plain,
( big_p(c11)
| ~ big_p(X7115)
| big_p(X7114)
| ~ big_q(c20) ),
inference(factor,[status(thm)],[c78419]) ).
cnf(c78423,plain,
( big_p(c11)
| ~ big_p(X7118)
| big_p(X7117)
| big_p(X7116) ),
inference(resolution,[status(thm)],[c78421,c78341]) ).
cnf(clause_4,negated_conjecture,
( big_p(X87)
| big_p(f1(X87))
| ~ big_q(X89)
| big_p(X88)
| ~ big_q(f2(X86))
| ~ big_q(X86)
| big_p(c6)
| ~ big_q(c7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_4) ).
cnf(c10,plain,
( big_p(X91)
| big_p(f1(X91))
| ~ big_q(f2(X90))
| big_p(X92)
| ~ big_q(X90)
| big_p(c6)
| ~ big_q(c7) ),
inference(factor,[status(thm)],[clause_4]) ).
cnf(c78401,plain,
( big_p(X9377)
| big_p(X9380)
| big_p(f1(X9380))
| big_p(X9379)
| ~ big_q(X9378)
| big_p(c6)
| ~ big_q(c7) ),
inference(resolution,[status(thm)],[c78341,c10]) ).
cnf(c78454,plain,
( big_p(X9383)
| big_p(X9382)
| big_p(f1(X9382))
| big_p(X9381)
| ~ big_q(c7)
| big_p(c6) ),
inference(factor,[status(thm)],[c78401]) ).
cnf(c78456,plain,
( big_p(X9390)
| big_p(X9392)
| big_p(f1(X9392))
| big_p(X9391)
| big_p(c6)
| big_p(X9389) ),
inference(resolution,[status(thm)],[c78454,c78341]) ).
cnf(c78457,plain,
( big_p(X9394)
| big_p(f1(X9394))
| big_p(X9393)
| big_p(c6)
| big_p(X9395) ),
inference(factor,[status(thm)],[c78456]) ).
cnf(c78515,plain,
( big_p(X9397)
| big_p(f1(X9397))
| big_p(c6)
| big_p(X9396) ),
inference(factor,[status(thm)],[c78457]) ).
cnf(c78559,plain,
( big_p(X9398)
| big_p(f1(X9398))
| big_p(c6) ),
inference(factor,[status(thm)],[c78515]) ).
cnf(c78587,plain,
( big_p(c6)
| big_p(f1(c6)) ),
inference(factor,[status(thm)],[c78559]) ).
cnf(c78604,plain,
( big_p(c6)
| big_p(c11)
| big_p(X9409)
| big_p(X9410) ),
inference(resolution,[status(thm)],[c78587,c78423]) ).
cnf(c78608,plain,
( big_p(c6)
| big_p(c11)
| big_p(X9411) ),
inference(factor,[status(thm)],[c78604]) ).
cnf(c78636,plain,
( big_p(c6)
| big_p(c11) ),
inference(factor,[status(thm)],[c78608]) ).
cnf(c78651,plain,
( big_p(c11)
| big_p(X9417)
| big_p(X9418) ),
inference(resolution,[status(thm)],[c78636,c78423]) ).
cnf(c78654,plain,
( big_p(c11)
| big_p(X9419) ),
inference(factor,[status(thm)],[c78651]) ).
cnf(c78676,plain,
big_p(c11),
inference(factor,[status(thm)],[c78654]) ).
cnf(c78687,plain,
( big_p(X9436)
| big_p(X9439)
| big_p(X9437)
| big_p(X9438) ),
inference(resolution,[status(thm)],[c78676,c78429]) ).
cnf(c78688,plain,
( big_p(X9440)
| big_p(X9441)
| big_p(X9442) ),
inference(factor,[status(thm)],[c78687]) ).
cnf(c78714,plain,
( big_p(X9443)
| big_p(X9444) ),
inference(factor,[status(thm)],[c78688]) ).
cnf(c78729,plain,
big_p(X9445),
inference(factor,[status(thm)],[c78714]) ).
cnf(clause_123,negated_conjecture,
( ~ big_p(X702)
| ~ big_p(f3(X702))
| ~ big_q(X704)
| ~ big_p(c15)
| big_q(X703)
| ~ big_q(c16)
| ~ big_p(X706)
| big_q(X705) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_123) ).
cnf(c99,plain,
( ~ big_p(X710)
| ~ big_p(f3(X710))
| ~ big_q(X708)
| ~ big_p(c15)
| big_q(X707)
| ~ big_q(c16)
| big_q(X709) ),
inference(factor,[status(thm)],[clause_123]) ).
cnf(c78740,plain,
( ~ big_p(X9658)
| ~ big_q(X9660)
| ~ big_p(c15)
| big_q(X9659)
| ~ big_q(c16)
| big_q(X9661) ),
inference(resolution,[status(thm)],[c78729,c99]) ).
cnf(c78742,plain,
( ~ big_p(X9663)
| ~ big_q(c16)
| ~ big_p(c15)
| big_q(X9664)
| big_q(X9662) ),
inference(factor,[status(thm)],[c78740]) ).
cnf(c78744,plain,
( ~ big_p(X9665)
| ~ big_q(c16)
| big_q(X9667)
| big_q(X9666) ),
inference(resolution,[status(thm)],[c78742,c78729]) ).
cnf(clause_121,negated_conjecture,
( ~ big_p(X691)
| ~ big_p(f3(X691))
| ~ big_q(X693)
| ~ big_p(c15)
| ~ big_q(X692)
| big_q(c16)
| ~ big_p(X695)
| big_q(X694) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_121) ).
cnf(c98,plain,
( ~ big_p(X698)
| ~ big_p(f3(X698))
| ~ big_q(X697)
| ~ big_p(c15)
| ~ big_q(X699)
| big_q(c16)
| big_q(X696) ),
inference(factor,[status(thm)],[clause_121]) ).
cnf(c76304,plain,
( big_q(c16)
| ~ big_p(X7053)
| ~ big_q(X7055)
| ~ big_p(c15)
| ~ big_q(X7056)
| big_q(X7054) ),
inference(resolution,[status(thm)],[c76131,c98]) ).
cnf(c78413,plain,
( big_q(c16)
| ~ big_p(X7062)
| ~ big_q(X7061)
| ~ big_p(c15)
| big_q(X7063) ),
inference(factor,[status(thm)],[c76304]) ).
cnf(c78415,plain,
( big_q(c16)
| ~ big_p(c15)
| ~ big_q(X7064)
| big_q(X7065) ),
inference(factor,[status(thm)],[c78413]) ).
cnf(clause_25,negated_conjecture,
( ~ big_p(X358)
| ~ big_p(f1(X358))
| big_q(c1)
| ~ big_p(c2)
| big_q(f2(X356))
| big_q(X356)
| ~ big_p(X359)
| big_q(X357) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_25) ).
cnf(c43,plain,
( ~ big_p(X360)
| ~ big_p(f1(X360))
| big_q(c1)
| ~ big_p(c2)
| big_q(f2(X362))
| big_q(X362)
| big_q(X361) ),
inference(factor,[status(thm)],[clause_25]) ).
cnf(c78738,plain,
( ~ big_p(X9747)
| big_q(c1)
| ~ big_p(c2)
| big_q(f2(X9746))
| big_q(X9746)
| big_q(X9745) ),
inference(resolution,[status(thm)],[c78729,c43]) ).
cnf(c78746,plain,
( ~ big_p(X9750)
| big_q(c1)
| big_q(f2(X9749))
| big_q(X9749)
| big_q(X9748) ),
inference(resolution,[status(thm)],[c78738,c78729]) ).
cnf(c78747,plain,
( big_q(c1)
| big_q(f2(X9751))
| big_q(X9751)
| big_q(X9752) ),
inference(resolution,[status(thm)],[c78746,c78729]) ).
cnf(c78749,plain,
( big_q(c1)
| big_q(f2(X9753))
| big_q(X9753) ),
inference(factor,[status(thm)],[c78747]) ).
cnf(c78769,plain,
( big_q(c1)
| big_q(f2(c1)) ),
inference(factor,[status(thm)],[c78749]) ).
cnf(c78783,plain,
( big_q(c1)
| big_q(c16)
| ~ big_p(c15)
| big_q(X9763) ),
inference(resolution,[status(thm)],[c78769,c78415]) ).
cnf(c78786,plain,
( big_q(c1)
| big_q(c16)
| big_q(X9769) ),
inference(resolution,[status(thm)],[c78783,c78729]) ).
cnf(c78787,plain,
( big_q(c1)
| big_q(c16) ),
inference(factor,[status(thm)],[c78786]) ).
cnf(c78800,plain,
( big_q(c16)
| ~ big_p(c15)
| big_q(X9770) ),
inference(resolution,[status(thm)],[c78787,c78415]) ).
cnf(c78805,plain,
( big_q(c16)
| big_q(X9771) ),
inference(resolution,[status(thm)],[c78800,c78729]) ).
cnf(c78806,plain,
big_q(c16),
inference(factor,[status(thm)],[c78805]) ).
cnf(c78812,plain,
( ~ big_p(X9777)
| big_q(X9776)
| big_q(X9778) ),
inference(resolution,[status(thm)],[c78806,c78744]) ).
cnf(c78813,plain,
( big_q(X9780)
| big_q(X9779) ),
inference(resolution,[status(thm)],[c78812,c78729]) ).
cnf(c78814,plain,
big_q(X9781),
inference(factor,[status(thm)],[c78813]) ).
cnf(clause_128,negated_conjecture,
( ~ big_p(X890)
| ~ big_p(f3(X890))
| ~ big_q(X891)
| ~ big_p(c15)
| ~ big_q(f4(X892))
| ~ big_q(X892)
| ~ big_p(X893)
| ~ big_q(c20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_128) ).
cnf(c1134,plain,
( ~ big_p(X894)
| ~ big_p(f3(X894))
| ~ big_q(f4(X896))
| ~ big_p(c15)
| ~ big_q(X896)
| ~ big_p(X895)
| ~ big_q(c20) ),
inference(factor,[status(thm)],[clause_128]) ).
cnf(c78817,plain,
( ~ big_p(X9904)
| ~ big_p(f3(X9904))
| ~ big_p(c15)
| ~ big_q(X9906)
| ~ big_p(X9905)
| ~ big_q(c20) ),
inference(resolution,[status(thm)],[c78814,c1134]) ).
cnf(c78819,plain,
( ~ big_p(X9908)
| ~ big_p(c15)
| ~ big_q(X9909)
| ~ big_p(X9907)
| ~ big_q(c20) ),
inference(resolution,[status(thm)],[c78817,c78729]) ).
cnf(c78821,plain,
( ~ big_p(X9917)
| ~ big_p(c15)
| ~ big_q(X9915)
| ~ big_p(X9916) ),
inference(resolution,[status(thm)],[c78819,c78814]) ).
cnf(c78822,plain,
( ~ big_p(X9919)
| ~ big_p(c15)
| ~ big_q(X9918) ),
inference(factor,[status(thm)],[c78821]) ).
cnf(c78825,plain,
( ~ big_p(X9920)
| ~ big_p(c15) ),
inference(resolution,[status(thm)],[c78822,c78814]) ).
cnf(c78827,plain,
~ big_p(X9921),
inference(resolution,[status(thm)],[c78825,c78729]) ).
cnf(c78828,plain,
$false,
inference(resolution,[status(thm)],[c78827,c78729]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SYN036-1 : TPTP v8.1.2. Released v1.0.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n005.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 19:51:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 104.59/104.84 % Version: 1.5
% 104.59/104.84 % SZS status Unsatisfiable
% 104.59/104.84 % SZS output start CNFRefutation
% See solution above
% 104.59/104.85
% 104.59/104.85 % Initial clauses : 128
% 104.59/104.85 % Processed clauses : 808
% 104.59/104.85 % Factors computed : 1248
% 104.59/104.85 % Resolvents computed: 77581
% 104.59/104.85 % Tautologies deleted: 175
% 104.59/104.85 % Forward subsumed : 2147
% 104.59/104.85 % Backward subsumed : 805
% 104.59/104.85 % -------- CPU Time ---------
% 104.59/104.85 % User time : 104.110 s
% 104.59/104.85 % System time : 0.319 s
% 104.59/104.85 % Total time : 104.429 s
%------------------------------------------------------------------------------