The cow is red. The cow is round. The cow needs the mouse. The cow visits the squirrel. The mouse eats the cow. The mouse eats the squirrel. The mouse needs the squirrel. The mouse visits the squirrel. The squirrel eats the mouse. The squirrel is red. If the cow visits the mouse and the cow eats the squirrel then the squirrel needs the mouse. If someone is red then they eat the cow. If someone eats the cow and they need the squirrel then the squirrel is young. If someone eats the mouse then they visit the cow. If the squirrel is young then the squirrel needs the mouse. If someone needs the mouse and the mouse needs the squirrel then they are nice.
The cow is red.
("cow" "is" "red" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
If the cow visits the mouse and the cow eats the squirrel then the squirrel needs the mouse.
((("cow" "visits" "mouse" "+") ("cow" "eats" "squirrel" "+")) -> ("squirrel" "needs" "mouse" "+"))
If someone is red then they eat the cow.
((("someone" "is" "red" "+")) -> ("someone" "eats" "cow" "+"))
If someone eats the cow and they need the squirrel then the squirrel is young.
((("someone" "eats" "cow" "+") ("someone" "needs" "squirrel" "+")) -> ("squirrel" "is" "young" "+"))
If someone eats the mouse then they visit the cow.
((("someone" "eats" "mouse" "+")) -> ("someone" "visits" "cow" "+"))
If the squirrel is young then the squirrel needs the mouse.
((("squirrel" "is" "young" "+")) -> ("squirrel" "needs" "mouse" "+"))
If someone needs the mouse and the mouse needs the squirrel then they are nice.
((("someone" "needs" "mouse" "+") ("mouse" "needs" "squirrel" "+")) -> ("someone" "is" "nice" "+"))
The mouse visits the squirrel.
True
1
proof
[(triple8)]
("mouse" "visits" "squirrel" "+")
triple8
The cow does not need the mouse.
False
1
inv-proof
[(triple3)]
("cow" "needs" "mouse" "-")
triple3
The squirrel is young.
True
3
proof
[(((triple5 triple7) -> rule3))]
("squirrel" "is" "young" "+")
((triple5 triple7) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel does not visit the cow.
False
2
inv-proof
[(((triple9) -> rule4))]
("squirrel" "visits" "cow" "-")
((triple9) -> (rule4 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel needs the mouse.
True
4
proof
[(((((triple5 triple7) -> rule3)) -> rule5))]
("squirrel" "needs" "mouse" "+")
((((triple5 triple7) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel does not need the mouse.
False
4
inv-proof
[(((((triple5 triple7) -> rule3)) -> rule5))]
("squirrel" "needs" "mouse" "-")
((((triple5 triple7) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is nice.
True
6
proof
[(((((((triple5 triple7) -> rule3)) -> rule5) triple7) -> rule6))]
("squirrel" "is" "nice" "+")
((((((triple5 triple7) -> (rule3 % int3))) -> (rule5 % int2)) triple7) -> (rule6 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
int3
The squirrel is not nice.
False
6
inv-proof
[(((((((triple5 triple7) -> rule3)) -> rule5) triple7) -> rule6))]
("squirrel" "is" "nice" "-")
((((((triple5 triple7) -> (rule3 % int3))) -> (rule5 % int2)) triple7) -> (rule6 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
int3
The mouse does not visit the cow.
Unknown
inv-rconc
[@1: The mouse visits the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "visits" "cow" "-")
The cow visits the cow.
Unknown
rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "visits" "cow" "+")
The mouse is not nice.
Unknown
inv-rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "nice" "-")
The cow eats the squirrel.
Unknown
random
[@0: The cow eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "squirrel" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The mouse needs the cow.
Unknown
random
[@0: The mouse needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cow" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
@0: The cow is red.[(triple1)] The cow is round.[(triple2)] The cow needs the mouse.[(triple3)] The cow visits the squirrel.[(triple4)] The mouse eats the cow.[(triple5)] The mouse eats the squirrel.[(triple6)] The mouse needs the squirrel.[(triple7)] The mouse visits the squirrel.[(triple8)] The squirrel eats the mouse.[(triple9)] The squirrel is red.[(triple10)] @1: The cow eats the cow.[(((triple1) -> rule2))] The cow is nice.[(((triple3 triple7) -> rule6))] The squirrel eats the cow.[(((triple10) -> rule2))] The squirrel is young.[(((triple5 triple7) -> rule3))] The squirrel visits the cow.[(((triple9) -> rule4))] @2: The squirrel needs the mouse.[(((((triple5 triple7) -> rule3)) -> rule5))] @3: The squirrel is nice.[(((((((triple5 triple7) -> rule3)) -> rule5) triple7) -> rule6))]
The cow is red.
("cow" "is" "red" "+")
triple1
The cow is round.
("cow" "is" "round" "+")
triple2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple3
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple4
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple5
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple6
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple7
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple8
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple9
The squirrel is red.
("squirrel" "is" "red" "+")
triple10
The cow eats the cow.
("cow" "eats" "cow" "+")
((triple1) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
((triple3 triple7) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
((triple10) -> (rule2 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
((triple5 triple7) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
((triple9) -> (rule4 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
((((triple5 triple7) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
((((((triple5 triple7) -> (rule3 % int3))) -> (rule5 % int2)) triple7) -> (rule6 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
int3