The cat needs the cow. The cat sees the lion. The cat visits the squirrel. The cow visits the squirrel. The lion needs the squirrel. The lion sees the squirrel. The squirrel is red. The squirrel is round. The squirrel visits the cat. The squirrel visits the lion. If something needs the squirrel and it visits the lion then it sees the lion. If something is cold then it sees the cat. If something sees the squirrel then the squirrel is cold.
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If something needs the squirrel and it visits the lion then it sees the lion.
((("something" "needs" "squirrel" "+") ("something" "visits" "lion" "+")) -> ("something" "sees" "lion" "+"))
If something is cold then it sees the cat.
((("something" "is" "cold" "+")) -> ("something" "sees" "cat" "+"))
If something sees the squirrel then the squirrel is cold.
((("something" "sees" "squirrel" "+")) -> ("squirrel" "is" "cold" "+"))
The cat visits the squirrel.
True
1
proof
[(triple3)]
("cat" "visits" "squirrel" "+")
triple3
The squirrel is not red.
False
1
inv-proof
[(triple7)]
("squirrel" "is" "red" "-")
triple7
The squirrel is cold.
True
2
proof
[(((triple6) -> rule3))]
("squirrel" "is" "cold" "+")
((triple6) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is not cold.
False
2
inv-proof
[(((triple6) -> rule3))]
("squirrel" "is" "cold" "-")
((triple6) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The cow does not see the cat.
Unknown
inv-rconc
[@1: The cow sees the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "sees" "cat" "-")
The cow sees the lion.
Unknown
rconc
[@1: The cow sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "lion" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The cat needs the cow.[(triple1)] The cat sees the lion.[(triple2)] The cat visits the squirrel.[(triple3)] The cow visits the squirrel.[(triple4)] The lion needs the squirrel.[(triple5)] The lion sees the squirrel.[(triple6)] The squirrel is red.[(triple7)] The squirrel is round.[(triple8)] The squirrel visits the cat.[(triple9)] The squirrel visits the lion.[(triple10)] @1: The squirrel is cold.[(((triple6) -> rule3))] @2: The squirrel sees the cat.[(((((triple6) -> rule3)) -> rule2))]
The cat needs the cow.
("cat" "needs" "cow" "+")
triple1
The cat sees the lion.
("cat" "sees" "lion" "+")
triple2
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple3
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple4
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple5
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple6
The squirrel is red.
("squirrel" "is" "red" "+")
triple7
The squirrel is round.
("squirrel" "is" "round" "+")
triple8
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple9
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple10
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple6) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2