The cow is red. The cow does not need the lion. The cow sees the lion. The cow sees the squirrel. The cow visits the squirrel. The lion is big. The lion is cold. The lion visits the squirrel. The squirrel is big. The squirrel is cold. If someone visits the lion and the lion does not visit the squirrel then the squirrel sees the lion. If the lion is young and the lion sees the squirrel then the squirrel sees the lion. If someone is rough then they see the squirrel. If someone needs the lion and they see the lion then they see the squirrel. If someone sees the lion then they do not visit the lion. If the cow sees the squirrel and the cow does not visit the lion then the squirrel does not see the cow.
The cow is red.
("cow" "is" "red" "+")
The cow does not need the lion.
("cow" "needs" "lion" "-")
The cow sees the lion.
("cow" "sees" "lion" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
If someone visits the lion and the lion does not visit the squirrel then the squirrel sees the lion.
((("someone" "visits" "lion" "+") ("lion" "visits" "squirrel" "~")) -> ("squirrel" "sees" "lion" "+"))
If the lion is young and the lion sees the squirrel then the squirrel sees the lion.
((("lion" "is" "young" "+") ("lion" "sees" "squirrel" "+")) -> ("squirrel" "sees" "lion" "+"))
If someone is rough then they see the squirrel.
((("someone" "is" "rough" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone needs the lion and they see the lion then they see the squirrel.
((("someone" "needs" "lion" "+") ("someone" "sees" "lion" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone sees the lion then they do not visit the lion.
((("someone" "sees" "lion" "+")) -> ("someone" "visits" "lion" "-"))
If the cow sees the squirrel and the cow does not visit the lion then the squirrel does not see the cow.
((("cow" "sees" "squirrel" "+") ("cow" "visits" "lion" "~")) -> ("squirrel" "sees" "cow" "-"))
The lion is cold.
True
1
proof
[(triple7)]
("lion" "is" "cold" "+")
triple7
The cow does not visit the squirrel.
False
1
inv-proof
[(triple5)]
("cow" "visits" "squirrel" "-")
triple5
The cow does not visit the lion.
True
2
proof
[(((triple3) -> rule5))]
("cow" "visits" "lion" "-")
((triple3) -> (rule5 % int1))
The cow does not visit the lion.
("cow" "visits" "lion" "-")
int1
The cow visits the lion.
False
2
inv-proof
[(((triple3) -> rule5))]
("cow" "visits" "lion" "+")
((triple3) -> (rule5 % int1))
The cow does not visit the lion.
("cow" "visits" "lion" "-")
int1
The squirrel does not see the cow.
True
4
proof
[(((triple4 ((triple3) -> rule5)) -> rule6))]
("squirrel" "sees" "cow" "-")
((triple4 ((triple3) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel does not see the cow.
("squirrel" "sees" "cow" "-")
int1
The cow does not visit the lion.
("cow" "visits" "lion" "-")
int2
The squirrel sees the cow.
False
4
inv-proof
[(((triple4 ((triple3) -> rule5)) -> rule6))]
("squirrel" "sees" "cow" "+")
((triple4 ((triple3) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel does not see the cow.
("squirrel" "sees" "cow" "-")
int1
The cow does not visit the lion.
("cow" "visits" "lion" "-")
int2
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The lion sees the squirrel.
Unknown
rconc
[@1: The lion sees the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "sees" "squirrel" "+")
The squirrel does not see the lion.
Unknown
inv-rconc
[@1: The squirrel sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "lion" "-")
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 cold.
Unknown
inv-random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "-")
The lion needs the squirrel.
Unknown
random
[@0: The lion needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "squirrel" "+")
@0: The cow does not need the lion.[(triple2)] The cow is red.[(triple1)] The cow sees the lion.[(triple3)] The cow sees the squirrel.[(triple4)] The cow visits the squirrel.[(triple5)] The lion is big.[(triple6)] The lion is cold.[(triple7)] The lion visits the squirrel.[(triple8)] The squirrel is big.[(triple9)] The squirrel is cold.[(triple10)] @1: The cow does not visit the lion.[(((triple3) -> rule5))] @2: The squirrel does not see the cow.[(((triple4 ((triple3) -> rule5)) -> rule6))]
The cow does not need the lion.
("cow" "needs" "lion" "-")
triple2
The cow is red.
("cow" "is" "red" "+")
triple1
The cow sees the lion.
("cow" "sees" "lion" "+")
triple3
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple4
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple5
The lion is big.
("lion" "is" "big" "+")
triple6
The lion is cold.
("lion" "is" "cold" "+")
triple7
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple8
The squirrel is big.
("squirrel" "is" "big" "+")
triple9
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple10
The cow does not visit the lion.
("cow" "visits" "lion" "-")
((triple3) -> (rule5 % int1))
The cow does not visit the lion.
("cow" "visits" "lion" "-")
int1
The squirrel does not see the cow.
("squirrel" "sees" "cow" "-")
((triple4 ((triple3) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel does not see the cow.
("squirrel" "sees" "cow" "-")
int1
The cow does not visit the lion.
("cow" "visits" "lion" "-")
int2