The cow is young. The cow needs the mouse. The mouse needs the cow. The squirrel visits the cow. The squirrel visits the tiger. The tiger is blue. The tiger is rough. The tiger needs the mouse. The tiger visits the mouse. The tiger visits the squirrel. If something is cold then it eats the squirrel. If something needs the tiger then it needs the cow. If something needs the tiger then it visits the tiger. If something is young and green then it visits the tiger. If something is blue then it eats the tiger. If something eats the cow then the cow is blue. If something visits the tiger then it needs the cow. If something eats the tiger then it is cold.
The cow is young.
("cow" "is" "young" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If something is cold then it eats the squirrel.
((("something" "is" "cold" "+")) -> ("something" "eats" "squirrel" "+"))
If something needs the tiger then it needs the cow.
((("something" "needs" "tiger" "+")) -> ("something" "needs" "cow" "+"))
If something needs the tiger then it visits the tiger.
((("something" "needs" "tiger" "+")) -> ("something" "visits" "tiger" "+"))
If something is young and green then it visits the tiger.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "visits" "tiger" "+"))
If something is blue then it eats the tiger.
((("something" "is" "blue" "+")) -> ("something" "eats" "tiger" "+"))
If something eats the cow then the cow is blue.
((("something" "eats" "cow" "+")) -> ("cow" "is" "blue" "+"))
If something visits the tiger then it needs the cow.
((("something" "visits" "tiger" "+")) -> ("something" "needs" "cow" "+"))
If something eats the tiger then it is cold.
((("something" "eats" "tiger" "+")) -> ("something" "is" "cold" "+"))
The cow needs the mouse.
True
1
proof
[(triple2)]
("cow" "needs" "mouse" "+")
triple2
The cow does not need the mouse.
False
1
inv-proof
[(triple2)]
("cow" "needs" "mouse" "-")
triple2
The tiger eats the tiger.
True
2
proof
[(((triple6) -> rule5))]
("tiger" "eats" "tiger" "+")
((triple6) -> (rule5 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The squirrel does not need the cow.
False
2
inv-proof
[(((triple5) -> rule7))]
("squirrel" "needs" "cow" "-")
((triple5) -> (rule7 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The tiger is cold.
True
3
proof
[(((((triple6) -> rule5)) -> rule8))]
("tiger" "is" "cold" "+")
((((triple6) -> (rule5 % int2))) -> (rule8 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger is not cold.
False
3
inv-proof
[(((((triple6) -> rule5)) -> rule8))]
("tiger" "is" "cold" "-")
((((triple6) -> (rule5 % int2))) -> (rule8 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger eats the squirrel.
True
4
proof
[(((((((triple6) -> rule5)) -> rule8)) -> rule1))]
("tiger" "eats" "squirrel" "+")
((((((triple6) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
The tiger does not eat the squirrel.
False
4
inv-proof
[(((((((triple6) -> rule5)) -> rule8)) -> rule1))]
("tiger" "eats" "squirrel" "-")
((((((triple6) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
The tiger does not visit the tiger.
Unknown
inv-rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The cow visits the tiger.
Unknown
rconc
[@1: The cow visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "visits" "tiger" "+")
The mouse does not eat the tiger.
Unknown
inv-rconc
[@1: The mouse eats the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "eats" "tiger" "-")
The mouse is cold.
Unknown
rconc
[@2: The mouse is cold.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("mouse" "is" "cold" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The mouse needs the tiger.
Unknown
random
[@0: The mouse needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "tiger" "+")
@0: The cow is young.[(triple1)] The cow needs the mouse.[(triple2)] The mouse needs the cow.[(triple3)] The squirrel visits the cow.[(triple4)] The squirrel visits the tiger.[(triple5)] The tiger is blue.[(triple6)] The tiger is rough.[(triple7)] The tiger needs the mouse.[(triple8)] The tiger visits the mouse.[(triple9)] The tiger visits the squirrel.[(triple10)] @1: The squirrel needs the cow.[(((triple5) -> rule7))] The tiger eats the tiger.[(((triple6) -> rule5))] @2: The tiger is cold.[(((((triple6) -> rule5)) -> rule8))] @3: The tiger eats the squirrel.[(((((((triple6) -> rule5)) -> rule8)) -> rule1))]
The cow is young.
("cow" "is" "young" "+")
triple1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple2
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple3
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple4
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple5
The tiger is blue.
("tiger" "is" "blue" "+")
triple6
The tiger is rough.
("tiger" "is" "rough" "+")
triple7
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple8
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple9
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple10
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
((triple5) -> (rule7 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple6) -> (rule5 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
((((triple6) -> (rule5 % int2))) -> (rule8 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
((((((triple6) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3