The cow chases the squirrel. The cow is not cold. The cow is green. The cow is nice. The cow does not visit the squirrel. The squirrel chases the cow. The squirrel is cold. The squirrel is green. The squirrel is kind. The squirrel is nice. The squirrel needs the cow. The squirrel visits the cow. If something needs the squirrel then it visits the squirrel. If the squirrel visits the cow and the squirrel chases the cow then the squirrel is red. If something is nice and red then it needs the squirrel.
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The cow is not cold.
("cow" "is" "cold" "-")
The cow is green.
("cow" "is" "green" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow does not visit the squirrel.
("cow" "visits" "squirrel" "-")
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
If something needs the squirrel then it visits the squirrel.
((("something" "needs" "squirrel" "+")) -> ("something" "visits" "squirrel" "+"))
If the squirrel visits the cow and the squirrel chases the cow then the squirrel is red.
((("squirrel" "visits" "cow" "+") ("squirrel" "chases" "cow" "+")) -> ("squirrel" "is" "red" "+"))
If something is nice and red then it needs the squirrel.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "needs" "squirrel" "+"))
The squirrel is nice.
True
1
proof
[(triple10)]
("squirrel" "is" "nice" "+")
triple10
The squirrel does not chase the cow.
False
1
inv-proof
[(triple6)]
("squirrel" "chases" "cow" "-")
triple6
The squirrel is red.
True
3
proof
[(((triple12 triple6) -> rule2))]
("squirrel" "is" "red" "+")
((triple12 triple6) -> (rule2 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is not red.
False
3
inv-proof
[(((triple12 triple6) -> rule2))]
("squirrel" "is" "red" "-")
((triple12 triple6) -> (rule2 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel needs the squirrel.
True
5
proof
[(((triple10 ((triple12 triple6) -> rule2)) -> rule3))]
("squirrel" "needs" "squirrel" "+")
((triple10 ((triple12 triple6) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel does not need the squirrel.
False
5
inv-proof
[(((triple10 ((triple12 triple6) -> rule2)) -> rule3))]
("squirrel" "needs" "squirrel" "-")
((triple10 ((triple12 triple6) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The cow does not need the squirrel.
Unknown
inv-rconc
[@1: The cow needs the squirrel.[CWA. Example of deepest failure = (rule3 <- 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" "+")
The cow is not red.
Unknown
inv-random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The cow chases the squirrel.[(triple1)] The cow does not visit the squirrel.[(triple5)] The cow is green.[(triple3)] The cow is nice.[(triple4)] The cow is not cold.[(triple2)] The squirrel chases the cow.[(triple6)] The squirrel is cold.[(triple7)] The squirrel is green.[(triple8)] The squirrel is kind.[(triple9)] The squirrel is nice.[(triple10)] The squirrel needs the cow.[(triple11)] The squirrel visits the cow.[(triple12)] @1: The squirrel is red.[(((triple12 triple6) -> rule2))] @2: The squirrel needs the squirrel.[(((triple10 ((triple12 triple6) -> rule2)) -> rule3))] @3: The squirrel visits the squirrel.[(((((triple10 ((triple12 triple6) -> rule2)) -> rule3)) -> rule1))]
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple1
The cow does not visit the squirrel.
("cow" "visits" "squirrel" "-")
triple5
The cow is green.
("cow" "is" "green" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
triple4
The cow is not cold.
("cow" "is" "cold" "-")
triple2
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
triple6
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple7
The squirrel is green.
("squirrel" "is" "green" "+")
triple8
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple9
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple10
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple11
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple12
The squirrel is red.
("squirrel" "is" "red" "+")
((triple12 triple6) -> (rule2 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((triple10 ((triple12 triple6) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((((triple10 ((triple12 triple6) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3