The cat is green. The cat visits the lion. The lion is round. The lion likes the cat. The lion likes the squirrel. The lion needs the mouse. The lion visits the mouse. The mouse likes the cat. The mouse needs the lion. The squirrel is round. The squirrel likes the cat. The squirrel visits the mouse. If someone is round then they need the cat. If someone likes the mouse and the mouse visits the lion then the mouse needs the squirrel. If someone is round and they need the cat then the cat is round.
The cat is green.
("cat" "is" "green" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If someone is round then they need the cat.
((("someone" "is" "round" "+")) -> ("someone" "needs" "cat" "+"))
If someone likes the mouse and the mouse visits the lion then the mouse needs the squirrel.
((("someone" "likes" "mouse" "+") ("mouse" "visits" "lion" "+")) -> ("mouse" "needs" "squirrel" "+"))
If someone is round and they need the cat then the cat is round.
((("someone" "is" "round" "+") ("someone" "needs" "cat" "+")) -> ("cat" "is" "round" "+"))
The lion is round.
True
1
proof
[(triple3)]
("lion" "is" "round" "+")
triple3
The lion does not like the squirrel.
False
1
inv-proof
[(triple5)]
("lion" "likes" "squirrel" "-")
triple5
The squirrel needs the cat.
True
2
proof
[(((triple10) -> rule1))]
("squirrel" "needs" "cat" "+")
((triple10) -> (rule1 % int1))
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int1
The lion does not need the cat.
False
2
inv-proof
[(((triple3) -> rule1))]
("lion" "needs" "cat" "-")
((triple3) -> (rule1 % int1))
The lion needs the cat.
("lion" "needs" "cat" "+")
int1
The cat is round.
True
4
proof
[(((triple10 ((triple10) -> rule1)) -> rule3) OR ((triple3 ((triple3) -> rule1)) -> rule3))]
("cat" "is" "round" "+")
((triple10 ((triple10) -> (rule1 % int2))) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int2
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The cat is not round.
False
4
inv-proof
[(((triple10 ((triple10) -> rule1)) -> rule3) OR ((triple3 ((triple3) -> rule1)) -> rule3))]
("cat" "is" "round" "-")
((triple10 ((triple10) -> (rule1 % int2))) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int2
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The cat needs the cat.
True
5
proof
[(((((triple10 ((triple10) -> rule1)) -> rule3)) -> rule1) OR ((((triple3 ((triple3) -> rule1)) -> rule3)) -> rule1))]
("cat" "needs" "cat" "+")
((((triple10 ((triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int3
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The lion needs the cat.
("lion" "needs" "cat" "+")
int3
The cat does not need the cat.
False
5
inv-proof
[(((((triple10 ((triple10) -> rule1)) -> rule3)) -> rule1) OR ((((triple3 ((triple3) -> rule1)) -> rule3)) -> rule1))]
("cat" "needs" "cat" "-")
((((triple10 ((triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int3
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The lion needs the cat.
("lion" "needs" "cat" "+")
int3
The mouse does not need the cat.
Unknown
inv-rconc
[@1: The mouse needs the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "needs" "cat" "-")
The mouse needs the squirrel.
Unknown
rconc
[@1: The mouse needs the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "needs" "squirrel" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The mouse likes the lion.
Unknown
random
[@0: The mouse likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "lion" "+")
The cat does not visit the mouse.
Unknown
inv-random
[@0: The cat visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "mouse" "-")
The squirrel likes the mouse.
Unknown
random
[@0: The squirrel likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "mouse" "+")
The mouse does not visit the lion.
Unknown
inv-random
[@0: The mouse visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "lion" "-")
The squirrel needs the mouse.
Unknown
random
[@0: The squirrel needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "mouse" "+")
@0: The cat is green.[(triple1)] The cat visits the lion.[(triple2)] The lion is round.[(triple3)] The lion likes the cat.[(triple4)] The lion likes the squirrel.[(triple5)] The lion needs the mouse.[(triple6)] The lion visits the mouse.[(triple7)] The mouse likes the cat.[(triple8)] The mouse needs the lion.[(triple9)] The squirrel is round.[(triple10)] The squirrel likes the cat.[(triple11)] The squirrel visits the mouse.[(triple12)] @1: The lion needs the cat.[(((triple3) -> rule1))] The squirrel needs the cat.[(((triple10) -> rule1))] @2: The cat is round.[(((triple10 ((triple10) -> rule1)) -> rule3) OR ((triple3 ((triple3) -> rule1)) -> rule3))] @3: The cat needs the cat.[(((((triple10 ((triple10) -> rule1)) -> rule3)) -> rule1) OR ((((triple3 ((triple3) -> rule1)) -> rule3)) -> rule1))]
The cat is green.
("cat" "is" "green" "+")
triple1
The cat visits the lion.
("cat" "visits" "lion" "+")
triple2
The lion is round.
("lion" "is" "round" "+")
triple3
The lion likes the cat.
("lion" "likes" "cat" "+")
triple4
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple5
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple6
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple7
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple8
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple9
The squirrel is round.
("squirrel" "is" "round" "+")
triple10
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple11
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple12
The lion needs the cat.
("lion" "needs" "cat" "+")
((triple3) -> (rule1 % int1))
The lion needs the cat.
("lion" "needs" "cat" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
((triple10) -> (rule1 % int1))
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
((triple10 ((triple10) -> (rule1 % int2))) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int2
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The lion needs the cat.
("lion" "needs" "cat" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
((((triple10 ((triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int3
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The lion needs the cat.
("lion" "needs" "cat" "+")
int3