The rabbit eats the squirrel. The rabbit eats the tiger. The rabbit is rough. The rabbit is young. The rabbit needs the squirrel. The squirrel chases the tiger. The squirrel eats the rabbit. The squirrel eats the tiger. The squirrel is green. The squirrel is rough. The squirrel needs the rabbit. The squirrel needs the tiger. The tiger chases the rabbit. The tiger eats the squirrel. The tiger is big. The tiger is nice. If the rabbit needs the squirrel then the squirrel needs the rabbit. If something eats the rabbit then it chases the rabbit. If the squirrel is nice and the squirrel eats the rabbit then the rabbit eats the squirrel. If something eats the tiger then it chases the squirrel. If something is rough then it chases the rabbit. If something chases the squirrel and the squirrel chases the tiger then the squirrel is rough.
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
If the rabbit needs the squirrel then the squirrel needs the rabbit.
((("rabbit" "needs" "squirrel" "+")) -> ("squirrel" "needs" "rabbit" "+"))
If something eats the rabbit then it chases the rabbit.
((("something" "eats" "rabbit" "+")) -> ("something" "chases" "rabbit" "+"))
If the squirrel is nice and the squirrel eats the rabbit then the rabbit eats the squirrel.
((("squirrel" "is" "nice" "+") ("squirrel" "eats" "rabbit" "+")) -> ("rabbit" "eats" "squirrel" "+"))
If something eats the tiger then it chases the squirrel.
((("something" "eats" "tiger" "+")) -> ("something" "chases" "squirrel" "+"))
If something is rough then it chases the rabbit.
((("something" "is" "rough" "+")) -> ("something" "chases" "rabbit" "+"))
If something chases the squirrel and the squirrel chases the tiger then the squirrel is rough.
((("something" "chases" "squirrel" "+") ("squirrel" "chases" "tiger" "+")) -> ("squirrel" "is" "rough" "+"))
The squirrel eats the rabbit.
True
1
proof
[(triple7)]
("squirrel" "eats" "rabbit" "+")
triple7
The squirrel does not eat the rabbit.
False
1
inv-proof
[(triple7)]
("squirrel" "eats" "rabbit" "-")
triple7
The squirrel chases the rabbit.
True
2
proof
[(((triple10) -> rule5) OR ((triple7) -> rule2) OR ((((((triple2) -> rule4) triple6) -> rule6)) -> rule5) OR ((((((triple8) -> rule4) triple6) -> rule6)) -> rule5))]
("squirrel" "chases" "rabbit" "+")
((triple10) -> (rule5 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
((triple7) -> (rule2 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
((((((triple2) -> (rule4 % int3)) triple6) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int3
((((((triple8) -> (rule4 % int3)) triple6) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The squirrel does not chase the rabbit.
False
2
inv-proof
[(((triple10) -> rule5) OR ((triple7) -> rule2) OR ((((((triple2) -> rule4) triple6) -> rule6)) -> rule5) OR ((((((triple8) -> rule4) triple6) -> rule6)) -> rule5))]
("squirrel" "chases" "rabbit" "-")
((triple10) -> (rule5 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
((triple7) -> (rule2 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
((((((triple2) -> (rule4 % int3)) triple6) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int3
((((((triple8) -> (rule4 % int3)) triple6) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The tiger does not chase the squirrel.
Unknown
inv-rconc
[@1: The tiger chases the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "chases" "squirrel" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
@0: The rabbit eats the squirrel.[(triple1)] The rabbit eats the tiger.[(triple2)] The rabbit is rough.[(triple3)] The rabbit is young.[(triple4)] The rabbit needs the squirrel.[(triple5)] The squirrel chases the tiger.[(triple6)] The squirrel eats the rabbit.[(triple7)] The squirrel eats the tiger.[(triple8)] The squirrel is green.[(triple9)] The squirrel is rough.[(triple10 OR ((((triple2) -> rule4) triple6) -> rule6) OR ((((triple8) -> rule4) triple6) -> rule6))] The squirrel needs the rabbit.[(triple11 OR ((triple5) -> rule1))] The squirrel needs the tiger.[(triple12)] The tiger chases the rabbit.[(triple13)] The tiger eats the squirrel.[(triple14)] The tiger is big.[(triple15)] The tiger is nice.[(triple16)] @1: The rabbit chases the rabbit.[(((triple3) -> rule5))] The rabbit chases the squirrel.[(((triple2) -> rule4))] The squirrel chases the rabbit.[(((triple10) -> rule5) OR ((triple7) -> rule2) OR ((((((triple2) -> rule4) triple6) -> rule6)) -> rule5) OR ((((((triple8) -> rule4) triple6) -> rule6)) -> rule5))] The squirrel chases the squirrel.[(((triple8) -> rule4))]
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple2
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple3
The rabbit is young.
("rabbit" "is" "young" "+")
triple4
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple5
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple6
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple7
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple8
The squirrel is green.
("squirrel" "is" "green" "+")
triple9
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple10
((((triple2) -> (rule4 % int2)) triple6) -> (rule6 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int2
((((triple8) -> (rule4 % int2)) triple6) -> (rule6 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple11
((triple5) -> (rule1 % int1))
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
int1
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple12
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple13
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple14
The tiger is big.
("tiger" "is" "big" "+")
triple15
The tiger is nice.
("tiger" "is" "nice" "+")
triple16
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple3) -> (rule5 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
((triple2) -> (rule4 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
((triple10) -> (rule5 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
((triple7) -> (rule2 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
((((((triple2) -> (rule4 % int3)) triple6) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int3
((((((triple8) -> (rule4 % int3)) triple6) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int3
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((triple8) -> (rule4 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1