The cat is rough. The cow sees the cat. The squirrel is round. If someone is young then they do not see the squirrel. If the squirrel needs the cow and the squirrel does not see the cow then the cow sees the squirrel. If the cat needs the cow then the cat is not young. If someone sees the cat then they need the squirrel. If someone visits the cow and the cow is not young then they are rough. If someone needs the squirrel then the squirrel needs the cow.
The cat is rough.
("cat" "is" "rough" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
If someone is young then they do not see the squirrel.
((("someone" "is" "young" "+")) -> ("someone" "sees" "squirrel" "-"))
If the squirrel needs the cow and the squirrel does not see the cow then the cow sees the squirrel.
((("squirrel" "needs" "cow" "+") ("squirrel" "sees" "cow" "~")) -> ("cow" "sees" "squirrel" "+"))
If the cat needs the cow then the cat is not young.
((("cat" "needs" "cow" "+")) -> ("cat" "is" "young" "-"))
If someone sees the cat then they need the squirrel.
((("someone" "sees" "cat" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone visits the cow and the cow is not young then they are rough.
((("someone" "visits" "cow" "+") ("cow" "is" "young" "~")) -> ("someone" "is" "rough" "+"))
If someone needs the squirrel then the squirrel needs the cow.
((("someone" "needs" "squirrel" "+")) -> ("squirrel" "needs" "cow" "+"))
The cat is rough.
True
1
proof
[(triple1)]
("cat" "is" "rough" "+")
triple1
The cat is not rough.
False
1
inv-proof
[(triple1)]
("cat" "is" "rough" "-")
triple1
The cow needs the squirrel.
True
2
proof
[(((triple2) -> rule4))]
("cow" "needs" "squirrel" "+")
((triple2) -> (rule4 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow does not need the squirrel.
False
2
inv-proof
[(((triple2) -> rule4))]
("cow" "needs" "squirrel" "-")
((triple2) -> (rule4 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The squirrel needs the cow.
True
3
proof
[(((((triple2) -> rule4)) -> rule6))]
("squirrel" "needs" "cow" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The squirrel does not need the cow.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule6))]
("squirrel" "needs" "cow" "-")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2
The cat does not need the squirrel.
Unknown
inv-rconc
[@1: The cat needs the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "needs" "squirrel" "-")
The squirrel is rough.
Unknown
rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "rough" "+")
The cow is not rough.
Unknown
inv-rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "rough" "-")
The cat visits the squirrel.
Unknown
random
[@0: The cat visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "squirrel" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
@0: The cat is rough.[(triple1)] The cow sees the cat.[(triple2)] The squirrel is round.[(triple3)] @1: The cow needs the squirrel.[(((triple2) -> rule4))] @2: The squirrel needs the cow.[(((((triple2) -> rule4)) -> rule6))]
The cat is rough.
("cat" "is" "rough" "+")
triple1
The cow sees the cat.
("cow" "sees" "cat" "+")
triple2
The squirrel is round.
("squirrel" "is" "round" "+")
triple3
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
((triple2) -> (rule4 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int2