The cow likes the squirrel. The squirrel is round. The squirrel likes the tiger. The tiger is blue. The tiger likes the cow. The tiger likes the squirrel. The tiger visits the cow. If someone visits the squirrel then they eat the tiger. If someone likes the tiger and the tiger is blue then they like the cow. If someone eats the cow and the cow is blue then they visit the cow. If someone eats the squirrel and they visit the cow then the cow is nice. If someone eats the tiger and the tiger visits the cow then they are young. If someone is blue then they visit the squirrel.
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If someone visits the squirrel then they eat the tiger.
((("someone" "visits" "squirrel" "+")) -> ("someone" "eats" "tiger" "+"))
If someone likes the tiger and the tiger is blue then they like the cow.
((("someone" "likes" "tiger" "+") ("tiger" "is" "blue" "+")) -> ("someone" "likes" "cow" "+"))
If someone eats the cow and the cow is blue then they visit the cow.
((("someone" "eats" "cow" "+") ("cow" "is" "blue" "+")) -> ("someone" "visits" "cow" "+"))
If someone eats the squirrel and they visit the cow then the cow is nice.
((("someone" "eats" "squirrel" "+") ("someone" "visits" "cow" "+")) -> ("cow" "is" "nice" "+"))
If someone eats the tiger and the tiger visits the cow then they are young.
((("someone" "eats" "tiger" "+") ("tiger" "visits" "cow" "+")) -> ("someone" "is" "young" "+"))
If someone is blue then they visit the squirrel.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "squirrel" "+"))
The squirrel likes the tiger.
True
1
proof
[(triple3)]
("squirrel" "likes" "tiger" "+")
triple3
The squirrel is not round.
False
1
inv-proof
[(triple2)]
("squirrel" "is" "round" "-")
triple2
The tiger visits the squirrel.
True
2
proof
[(((triple4) -> rule6))]
("tiger" "visits" "squirrel" "+")
((triple4) -> (rule6 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger does not visit the squirrel.
False
2
inv-proof
[(((triple4) -> rule6))]
("tiger" "visits" "squirrel" "-")
((triple4) -> (rule6 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger eats the tiger.
True
3
proof
[(((((triple4) -> rule6)) -> rule1))]
("tiger" "eats" "tiger" "+")
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger does not eat the tiger.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule1))]
("tiger" "eats" "tiger" "-")
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger is young.
True
5
proof
[(((((((triple4) -> rule6)) -> rule1) triple7) -> rule5))]
("tiger" "is" "young" "+")
((((((triple4) -> (rule6 % int3))) -> (rule1 % int2)) triple7) -> (rule5 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int3
The tiger is not young.
False
5
inv-proof
[(((((((triple4) -> rule6)) -> rule1) triple7) -> rule5))]
("tiger" "is" "young" "-")
((((((triple4) -> (rule6 % int3))) -> (rule1 % int2)) triple7) -> (rule5 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int3
The cow does not visit the squirrel.
Unknown
inv-rconc
[@1: The cow visits the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "visits" "squirrel" "-")
The squirrel eats the tiger.
Unknown
rconc
[@2: The squirrel eats the tiger.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("squirrel" "eats" "tiger" "+")
The cow is not young.
Unknown
inv-rconc
[@3: The cow is young.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule6 <- FAIL)]]
("cow" "is" "young" "-")
The squirrel is young.
Unknown
rconc
[@3: The squirrel is young.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule6 <- FAIL)]]
("squirrel" "is" "young" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The squirrel is not nice.
Unknown
inv-random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
@0: The cow likes the squirrel.[(triple1)] The squirrel is round.[(triple2)] The squirrel likes the tiger.[(triple3)] The tiger is blue.[(triple4)] The tiger likes the cow.[(triple5)] The tiger likes the squirrel.[(triple6)] The tiger visits the cow.[(triple7)] @1: The squirrel likes the cow.[(((triple3 triple4) -> rule2))] The tiger visits the squirrel.[(((triple4) -> rule6))] @2: The tiger eats the tiger.[(((((triple4) -> rule6)) -> rule1))] @3: The tiger is young.[(((((((triple4) -> rule6)) -> rule1) triple7) -> rule5))]
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple1
The squirrel is round.
("squirrel" "is" "round" "+")
triple2
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple3
The tiger is blue.
("tiger" "is" "blue" "+")
triple4
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple5
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple6
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple7
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
((triple3 triple4) -> (rule2 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
((triple4) -> (rule6 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
((((((triple4) -> (rule6 % int3))) -> (rule1 % int2)) triple7) -> (rule5 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int3