The cat is round. The cat visits the squirrel. The cat visits the tiger. The squirrel eats the cat. The squirrel eats the tiger. The squirrel sees the cat. The tiger eats the cat. The tiger is not rough. The tiger visits the cat. The tiger visits the squirrel. If someone eats the tiger then the tiger eats the squirrel. If someone eats the tiger and the tiger eats the cat then they visit the cat.
The cat is round.
("cat" "is" "round" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger is not rough.
("tiger" "is" "rough" "-")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If someone eats the tiger then the tiger eats the squirrel.
((("someone" "eats" "tiger" "+")) -> ("tiger" "eats" "squirrel" "+"))
If someone eats the tiger and the tiger eats the cat then they visit the cat.
((("someone" "eats" "tiger" "+") ("tiger" "eats" "cat" "+")) -> ("someone" "visits" "cat" "+"))
The squirrel eats the cat.
True
1
proof
[(triple4)]
("squirrel" "eats" "cat" "+")
triple4
The tiger does not eat the cat.
False
1
inv-proof
[(triple7)]
("tiger" "eats" "cat" "-")
triple7
The squirrel visits the cat.
True
3
proof
[(((triple5 triple7) -> rule2))]
("squirrel" "visits" "cat" "+")
((triple5 triple7) -> (rule2 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The squirrel does not visit the cat.
False
3
inv-proof
[(((triple5 triple7) -> rule2))]
("squirrel" "visits" "cat" "-")
((triple5 triple7) -> (rule2 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The cat does not visit the cat.
Unknown
inv-rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "visits" "cat" "-")
The squirrel visits the tiger.
Unknown
random
[@0: The squirrel visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "tiger" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
@0: The cat is round.[(triple1)] The cat visits the squirrel.[(triple2)] The cat visits the tiger.[(triple3)] The squirrel eats the cat.[(triple4)] The squirrel eats the tiger.[(triple5)] The squirrel sees the cat.[(triple6)] The tiger eats the cat.[(triple7)] The tiger is not rough.[(triple8)] The tiger visits the cat.[(triple9)] The tiger visits the squirrel.[(triple10)] @1: The squirrel visits the cat.[(((triple5 triple7) -> rule2))] The tiger eats the squirrel.[(((triple5) -> rule1))]
The cat is round.
("cat" "is" "round" "+")
triple1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple3
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple4
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple5
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple6
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple7
The tiger is not rough.
("tiger" "is" "rough" "-")
triple8
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple9
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple10
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
((triple5 triple7) -> (rule2 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
((triple5) -> (rule1 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1