The cow is cold. The cow likes the mouse. The mouse visits the squirrel. The mouse visits the tiger. The squirrel is big. The squirrel is round. The squirrel likes the mouse. The squirrel likes the tiger. The tiger is blue. The tiger needs the mouse. The tiger visits the cow. The tiger visits the mouse. If someone is round and they like the tiger then they visit the tiger. If someone needs the cow then the cow is cold. If someone visits the tiger and they are blue then they need the squirrel. If someone visits the mouse then they need the cow. If someone is round then they like the tiger. If someone likes the mouse then they need the squirrel. If someone is round then they like the cow. If someone visits the mouse then the mouse needs the tiger. If someone needs the cow and they visit the cow then they are round.
The cow is cold.
("cow" "is" "cold" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone is round and they like the tiger then they visit the tiger.
((("someone" "is" "round" "+") ("someone" "likes" "tiger" "+")) -> ("someone" "visits" "tiger" "+"))
If someone needs the cow then the cow is cold.
((("someone" "needs" "cow" "+")) -> ("cow" "is" "cold" "+"))
If someone visits the tiger and they are blue then they need the squirrel.
((("someone" "visits" "tiger" "+") ("someone" "is" "blue" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone visits the mouse then they need the cow.
((("someone" "visits" "mouse" "+")) -> ("someone" "needs" "cow" "+"))
If someone is round then they like the tiger.
((("someone" "is" "round" "+")) -> ("someone" "likes" "tiger" "+"))
If someone likes the mouse then they need the squirrel.
((("someone" "likes" "mouse" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone is round then they like the cow.
((("someone" "is" "round" "+")) -> ("someone" "likes" "cow" "+"))
If someone visits the mouse then the mouse needs the tiger.
((("someone" "visits" "mouse" "+")) -> ("mouse" "needs" "tiger" "+"))
If someone needs the cow and they visit the cow then they are round.
((("someone" "needs" "cow" "+") ("someone" "visits" "cow" "+")) -> ("someone" "is" "round" "+"))
The tiger visits the mouse.
True
1
proof
[(triple12)]
("tiger" "visits" "mouse" "+")
triple12
The squirrel does not like the mouse.
False
1
inv-proof
[(triple7)]
("squirrel" "likes" "mouse" "-")
triple7
The squirrel visits the tiger.
True
3
proof
[(((triple6 triple8) -> rule1) OR ((triple6 ((triple6) -> rule5)) -> rule1))]
("squirrel" "visits" "tiger" "+")
((triple6 triple8) -> (rule1 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
((triple6 ((triple6) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int2
The squirrel does not need the squirrel.
False
2
inv-proof
[(((triple7) -> rule6))]
("squirrel" "needs" "squirrel" "-")
((triple7) -> (rule6 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The tiger is round.
True
4
proof
[(((((triple12) -> rule4) triple11) -> rule9))]
("tiger" "is" "round" "+")
((((triple12) -> (rule4 % int2)) triple11) -> (rule9 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger is not round.
False
4
inv-proof
[(((((triple12) -> rule4) triple11) -> rule9))]
("tiger" "is" "round" "-")
((((triple12) -> (rule4 % int2)) triple11) -> (rule9 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger likes the tiger.
True
5
proof
[(((((((triple12) -> rule4) triple11) -> rule9)) -> rule5))]
("tiger" "likes" "tiger" "+")
((((((triple12) -> (rule4 % int3)) triple11) -> (rule9 % int2))) -> (rule5 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int3
The tiger does not like the tiger.
False
5
inv-proof
[(((((((triple12) -> rule4) triple11) -> rule9)) -> rule5))]
("tiger" "likes" "tiger" "-")
((((((triple12) -> (rule4 % int3)) triple11) -> (rule9 % int2))) -> (rule5 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int3
The tiger visits the tiger.
True
10
proof
[(((((((triple12) -> rule4) triple11) -> rule9) ((((((triple12) -> rule4) triple11) -> rule9)) -> rule5)) -> rule1))]
("tiger" "visits" "tiger" "+")
((((((triple12) -> (rule4 % int4)) triple11) -> (rule9 % int3)) ((((((triple12) -> (rule4 % int4)) triple11) -> (rule9 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int4
The tiger does not visit the tiger.
False
10
inv-proof
[(((((((triple12) -> rule4) triple11) -> rule9) ((((((triple12) -> rule4) triple11) -> rule9)) -> rule5)) -> rule1))]
("tiger" "visits" "tiger" "-")
((((((triple12) -> (rule4 % int4)) triple11) -> (rule9 % int3)) ((((((triple12) -> (rule4 % int4)) triple11) -> (rule9 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int4
The tiger needs the squirrel.
True
12
proof
[(((((((((triple12) -> rule4) triple11) -> rule9) ((((((triple12) -> rule4) triple11) -> rule9)) -> rule5)) -> rule1) triple9) -> rule3))]
("tiger" "needs" "squirrel" "+")
((((((((triple12) -> (rule4 % int5)) triple11) -> (rule9 % int4)) ((((((triple12) -> (rule4 % int5)) triple11) -> (rule9 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) triple9) -> (rule3 % int1))
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger is round.
("tiger" "is" "round" "+")
int4
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int5
The tiger does not need the squirrel.
False
12
inv-proof
[(((((((((triple12) -> rule4) triple11) -> rule9) ((((((triple12) -> rule4) triple11) -> rule9)) -> rule5)) -> rule1) triple9) -> rule3))]
("tiger" "needs" "squirrel" "-")
((((((((triple12) -> (rule4 % int5)) triple11) -> (rule9 % int4)) ((((((triple12) -> (rule4 % int5)) triple11) -> (rule9 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) triple9) -> (rule3 % int1))
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger is round.
("tiger" "is" "round" "+")
int4
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int5
The cow does not visit the tiger.
Unknown
inv-rconc
[@2: The cow visits the tiger.[CWA. Example of deepest failure = (rule1 <- rule9 <- FAIL)]]
("cow" "visits" "tiger" "-")
The cow likes the tiger.
Unknown
rconc
[@2: The cow likes the tiger.[CWA. Example of deepest failure = (rule5 <- rule9 <- FAIL)]]
("cow" "likes" "tiger" "+")
The squirrel does not need the cow.
Unknown
inv-rconc
[@1: The squirrel needs the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "needs" "cow" "-")
The mouse likes the tiger.
Unknown
rconc
[@2: The mouse likes the tiger.[CWA. Example of deepest failure = (rule5 <- rule9 <- FAIL)]]
("mouse" "likes" "tiger" "+")
The mouse is not round.
Unknown
inv-rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("mouse" "is" "round" "-")
The cow needs the cow.
Unknown
rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "needs" "cow" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The squirrel does not visit the cow.
Unknown
inv-random
[@0: The squirrel visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "cow" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The cow is cold.[(triple1 OR ((((triple12) -> rule4)) -> rule2))] The cow likes the mouse.[(triple2)] The mouse visits the squirrel.[(triple3)] The mouse visits the tiger.[(triple4)] The squirrel is big.[(triple5)] The squirrel is round.[(triple6)] The squirrel likes the mouse.[(triple7)] The squirrel likes the tiger.[(triple8 OR ((triple6) -> rule5))] The tiger is blue.[(triple9)] The tiger needs the mouse.[(triple10)] The tiger visits the cow.[(triple11)] The tiger visits the mouse.[(triple12)] @1: The cow needs the squirrel.[(((triple2) -> rule6))] The mouse needs the tiger.[(((triple12) -> rule8))] The squirrel likes the cow.[(((triple6) -> rule7))] The squirrel needs the squirrel.[(((triple7) -> rule6))] The squirrel visits the tiger.[(((triple6 triple8) -> rule1) OR ((triple6 ((triple6) -> rule5)) -> rule1))] The tiger needs the cow.[(((triple12) -> rule4))] @2: The tiger is round.[(((((triple12) -> rule4) triple11) -> rule9))] @3: The tiger likes the cow.[(((((((triple12) -> rule4) triple11) -> rule9)) -> rule7))] The tiger likes the tiger.[(((((((triple12) -> rule4) triple11) -> rule9)) -> rule5))] @4: The tiger visits the tiger.[(((((((triple12) -> rule4) triple11) -> rule9) ((((((triple12) -> rule4) triple11) -> rule9)) -> rule5)) -> rule1))] @5: The tiger needs the squirrel.[(((((((((triple12) -> rule4) triple11) -> rule9) ((((((triple12) -> rule4) triple11) -> rule9)) -> rule5)) -> rule1) triple9) -> rule3))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
((((triple12) -> (rule4 % int2))) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple3
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple4
The squirrel is big.
("squirrel" "is" "big" "+")
triple5
The squirrel is round.
("squirrel" "is" "round" "+")
triple6
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple7
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple8
((triple6) -> (rule5 % int1))
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple10
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple11
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple12
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
((triple2) -> (rule6 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
((triple12) -> (rule8 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
((triple6) -> (rule7 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((triple7) -> (rule6 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
((triple6 triple8) -> (rule1 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
((triple6 ((triple6) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
((triple12) -> (rule4 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
((((triple12) -> (rule4 % int2)) triple11) -> (rule9 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
((((((triple12) -> (rule4 % int3)) triple11) -> (rule9 % int2))) -> (rule7 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int3
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((((triple12) -> (rule4 % int3)) triple11) -> (rule9 % int2))) -> (rule5 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int3
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((((((triple12) -> (rule4 % int4)) triple11) -> (rule9 % int3)) ((((((triple12) -> (rule4 % int4)) triple11) -> (rule9 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int4
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
((((((((triple12) -> (rule4 % int5)) triple11) -> (rule9 % int4)) ((((((triple12) -> (rule4 % int5)) triple11) -> (rule9 % int4))) -> (rule5 % int3))) -> (rule1 % int2)) triple9) -> (rule3 % int1))
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger is round.
("tiger" "is" "round" "+")
int4
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int5