The cow eats the squirrel. The cow is blue. The cow is cold. The cow sees the squirrel. The squirrel eats the cow. The squirrel is rough. The squirrel needs the cow. If the cow is blue then the cow is nice. If something needs the cow and the cow sees the squirrel then it is nice. Red things are nice. If something needs the cow then it is blue. If something eats the squirrel then the squirrel is nice. All nice things are cold. If something sees the cow then the cow is nice. If something needs the cow and the cow is cold then it eats the cow.
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
If the cow is blue then the cow is nice.
((("cow" "is" "blue" "+")) -> ("cow" "is" "nice" "+"))
If something needs the cow and the cow sees the squirrel then it is nice.
((("something" "needs" "cow" "+") ("cow" "sees" "squirrel" "+")) -> ("something" "is" "nice" "+"))
Red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If something needs the cow then it is blue.
((("something" "needs" "cow" "+")) -> ("something" "is" "blue" "+"))
If something eats the squirrel then the squirrel is nice.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "is" "nice" "+"))
All nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something sees the cow then the cow is nice.
((("something" "sees" "cow" "+")) -> ("cow" "is" "nice" "+"))
If something needs the cow and the cow is cold then it eats the cow.
((("something" "needs" "cow" "+") ("cow" "is" "cold" "+")) -> ("something" "eats" "cow" "+"))
The cow eats the squirrel.
True
1
proof
[(triple1)]
("cow" "eats" "squirrel" "+")
triple1
The squirrel does not eat the cow.
False
1
inv-proof
[(triple5 OR ((triple7 triple3) -> rule8) OR ((triple7 ((((triple2) -> rule1)) -> rule6)) -> rule8))]
("squirrel" "eats" "cow" "-")
triple5
((triple7 triple3) -> (rule8 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
((triple7 ((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The cow is nice.
True
2
proof
[(((triple2) -> rule1))]
("cow" "is" "nice" "+")
((triple2) -> (rule1 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is not nice.
False
2
inv-proof
[(((triple2) -> rule1))]
("cow" "is" "nice" "-")
((triple2) -> (rule1 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The squirrel is cold.
True
3
proof
[(((((triple1) -> rule5)) -> rule6) OR ((((triple7 triple4) -> rule2)) -> rule6))]
("squirrel" "is" "cold" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
((((triple7 triple4) -> (rule2 % int2))) -> (rule6 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is not cold.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule6) OR ((((triple7 triple4) -> rule2)) -> rule6))]
("squirrel" "is" "cold" "-")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
((((triple7 triple4) -> (rule2 % int2))) -> (rule6 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The cow does not eat the cow.
Unknown
inv-rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "eats" "cow" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
The cow does not need the squirrel.
Unknown
inv-random
[@0: The cow needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "squirrel" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow eats the squirrel.[(triple1)] The cow is blue.[(triple2)] The cow is cold.[(triple3 OR ((((triple2) -> rule1)) -> rule6))] The cow sees the squirrel.[(triple4)] The squirrel eats the cow.[(triple5 OR ((triple7 triple3) -> rule8) OR ((triple7 ((((triple2) -> rule1)) -> rule6)) -> rule8))] The squirrel is rough.[(triple6)] The squirrel needs the cow.[(triple7)] @1: The cow is nice.[(((triple2) -> rule1))] The squirrel is blue.[(((triple7) -> rule4))] The squirrel is nice.[(((triple1) -> rule5) OR ((triple7 triple4) -> rule2))] @2: The squirrel is cold.[(((((triple1) -> rule5)) -> rule6) OR ((((triple7 triple4) -> rule2)) -> rule6))]
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow is cold.
("cow" "is" "cold" "+")
triple3
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple4
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple5
((triple7 triple3) -> (rule8 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
((triple7 ((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple6
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple7
The cow is nice.
("cow" "is" "nice" "+")
((triple2) -> (rule1 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
((triple7) -> (rule4 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
((triple1) -> (rule5 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((triple7 triple4) -> (rule2 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
((((triple7 triple4) -> (rule2 % int2))) -> (rule6 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2