The cat eats the lion. The cat eats the mouse. The lion does not eat the cat. The lion is nice. The lion is rough. The lion visits the mouse. The mouse is rough. The mouse needs the cat. The mouse needs the lion. The squirrel visits the cat. If someone is nice and rough then they need the lion. If someone visits the cat and the cat needs the lion then they need the lion. If someone is rough then they visit the cat. If someone needs the cat and they eat the squirrel then the cat does not eat the squirrel. If someone is cold then they do not need the mouse. If someone visits the squirrel then they are nice. If someone needs the squirrel and they are nice then they are rough. If someone is rough and they visit the cat then the cat needs the lion.
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The lion does not eat the cat.
("lion" "eats" "cat" "-")
The lion is nice.
("lion" "is" "nice" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
If someone is nice and rough then they need the lion.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "needs" "lion" "+"))
If someone visits the cat and the cat needs the lion then they need the lion.
((("someone" "visits" "cat" "+") ("cat" "needs" "lion" "+")) -> ("someone" "needs" "lion" "+"))
If someone is rough then they visit the cat.
((("someone" "is" "rough" "+")) -> ("someone" "visits" "cat" "+"))
If someone needs the cat and they eat the squirrel then the cat does not eat the squirrel.
((("someone" "needs" "cat" "+") ("someone" "eats" "squirrel" "+")) -> ("cat" "eats" "squirrel" "-"))
If someone is cold then they do not need the mouse.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "mouse" "-"))
If someone visits the squirrel then they are nice.
((("someone" "visits" "squirrel" "+")) -> ("someone" "is" "nice" "+"))
If someone needs the squirrel and they are nice then they are rough.
((("someone" "needs" "squirrel" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough and they visit the cat then the cat needs the lion.
((("someone" "is" "rough" "+") ("someone" "visits" "cat" "+")) -> ("cat" "needs" "lion" "+"))
The lion is nice.
True
1
proof
[(triple4)]
("lion" "is" "nice" "+")
triple4
The mouse does not need the cat.
False
1
inv-proof
[(triple8)]
("mouse" "needs" "cat" "-")
triple8
The lion visits the cat.
True
2
proof
[(((triple5) -> rule3))]
("lion" "visits" "cat" "+")
((triple5) -> (rule3 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion does not visit the cat.
False
2
inv-proof
[(((triple5) -> rule3))]
("lion" "visits" "cat" "-")
((triple5) -> (rule3 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The cat needs the lion.
True
4
proof
[(((triple5 ((triple5) -> rule3)) -> rule8) OR ((triple7 ((triple7) -> rule3)) -> rule8))]
("cat" "needs" "lion" "+")
((triple5 ((triple5) -> (rule3 % int2))) -> (rule8 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
((triple7 ((triple7) -> (rule3 % int2))) -> (rule8 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int2
The cat does not need the lion.
False
4
inv-proof
[(((triple5 ((triple5) -> rule3)) -> rule8) OR ((triple7 ((triple7) -> rule3)) -> rule8))]
("cat" "needs" "lion" "-")
((triple5 ((triple5) -> (rule3 % int2))) -> (rule8 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
((triple7 ((triple7) -> (rule3 % int2))) -> (rule8 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int2
The squirrel needs the lion.
True
6
proof
[(((triple10 ((triple5 ((triple5) -> rule3)) -> rule8)) -> rule2) OR ((triple10 ((triple7 ((triple7) -> rule3)) -> rule8)) -> rule2))]
("squirrel" "needs" "lion" "+")
((triple10 ((triple5 ((triple5) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
((triple10 ((triple7 ((triple7) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int3
The squirrel does not need the lion.
False
6
inv-proof
[(((triple10 ((triple5 ((triple5) -> rule3)) -> rule8)) -> rule2) OR ((triple10 ((triple7 ((triple7) -> rule3)) -> rule8)) -> rule2))]
("squirrel" "needs" "lion" "-")
((triple10 ((triple5 ((triple5) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
((triple10 ((triple7 ((triple7) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int3
The cat is not nice.
Unknown
inv-rconc
[@1: The cat is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "nice" "-")
The mouse is nice.
Unknown
rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "nice" "+")
The cat does not visit the cat.
Unknown
inv-rconc
[@2: The cat visits the cat.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("cat" "visits" "cat" "-")
The squirrel is rough.
Unknown
rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "is" "rough" "+")
The squirrel does not visit the mouse.
Unknown
inv-random
[@0: The squirrel visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "mouse" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The cat visits the squirrel.
Unknown
random
[@0: The cat visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "squirrel" "+")
@0: The cat eats the lion.[(triple1)] The cat eats the mouse.[(triple2)] The lion does not eat the cat.[(triple3)] The lion is nice.[(triple4)] The lion is rough.[(triple5)] The lion visits the mouse.[(triple6)] The mouse is rough.[(triple7)] The mouse needs the cat.[(triple8)] The mouse needs the lion.[(triple9 OR ((((triple7) -> rule3) ((triple5 ((triple5) -> rule3)) -> rule8)) -> rule2) OR ((((triple7) -> rule3) ((triple7 ((triple7) -> rule3)) -> rule8)) -> rule2))] The squirrel visits the cat.[(triple10)] @1: The lion needs the lion.[(((triple4 triple5) -> rule1) OR ((((triple5) -> rule3) ((triple5 ((triple5) -> rule3)) -> rule8)) -> rule2) OR ((((triple5) -> rule3) ((triple7 ((triple7) -> rule3)) -> rule8)) -> rule2))] The lion visits the cat.[(((triple5) -> rule3))] The mouse visits the cat.[(((triple7) -> rule3))] @2: The cat needs the lion.[(((triple5 ((triple5) -> rule3)) -> rule8) OR ((triple7 ((triple7) -> rule3)) -> rule8))] @3: The squirrel needs the lion.[(((triple10 ((triple5 ((triple5) -> rule3)) -> rule8)) -> rule2) OR ((triple10 ((triple7 ((triple7) -> rule3)) -> rule8)) -> rule2))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple2
The lion does not eat the cat.
("lion" "eats" "cat" "-")
triple3
The lion is nice.
("lion" "is" "nice" "+")
triple4
The lion is rough.
("lion" "is" "rough" "+")
triple5
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple6
The mouse is rough.
("mouse" "is" "rough" "+")
triple7
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple8
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple9
((((triple7) -> (rule3 % int4)) ((triple5 ((triple5) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int4
((((triple7) -> (rule3 % int3)) ((triple7 ((triple7) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int3
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple10
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple4 triple5) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
((((triple5) -> (rule3 % int3)) ((triple5 ((triple5) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
((((triple5) -> (rule3 % int4)) ((triple7 ((triple7) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int3
The lion visits the cat.
("lion" "visits" "cat" "+")
int4
The lion visits the cat.
("lion" "visits" "cat" "+")
((triple5) -> (rule3 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
((triple7) -> (rule3 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
((triple5 ((triple5) -> (rule3 % int2))) -> (rule8 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
((triple7 ((triple7) -> (rule3 % int2))) -> (rule8 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int2
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
((triple10 ((triple5 ((triple5) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
((triple10 ((triple7 ((triple7) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int3