The cat is cold. The cow chases the squirrel. The squirrel visits the cow. If something chases the cat and it needs the cow then it is young. If something is red then it is rough. If the squirrel visits the cat and the squirrel needs the cat then the squirrel chases the cat. If something is rough then it visits the cat. If something is red then it chases the squirrel. If the squirrel visits the cow then the squirrel needs the cow. If something visits the cow then it is rough. If the squirrel visits the cat then the cat is blue.
The cat is cold.
("cat" "is" "cold" "+")
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
If something chases the cat and it needs the cow then it is young.
((("something" "chases" "cat" "+") ("something" "needs" "cow" "+")) -> ("something" "is" "young" "+"))
If something is red then it is rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If the squirrel visits the cat and the squirrel needs the cat then the squirrel chases the cat.
((("squirrel" "visits" "cat" "+") ("squirrel" "needs" "cat" "+")) -> ("squirrel" "chases" "cat" "+"))
If something is rough then it visits the cat.
((("something" "is" "rough" "+")) -> ("something" "visits" "cat" "+"))
If something is red then it chases the squirrel.
((("something" "is" "red" "+")) -> ("something" "chases" "squirrel" "+"))
If the squirrel visits the cow then the squirrel needs the cow.
((("squirrel" "visits" "cow" "+")) -> ("squirrel" "needs" "cow" "+"))
If something visits the cow then it is rough.
((("something" "visits" "cow" "+")) -> ("something" "is" "rough" "+"))
If the squirrel visits the cat then the cat is blue.
((("squirrel" "visits" "cat" "+")) -> ("cat" "is" "blue" "+"))
The cat is cold.
True
1
proof
[(triple1)]
("cat" "is" "cold" "+")
triple1
The squirrel does not visit the cow.
False
1
inv-proof
[(triple3)]
("squirrel" "visits" "cow" "-")
triple3
The squirrel is rough.
True
2
proof
[(((triple3) -> rule7))]
("squirrel" "is" "rough" "+")
((triple3) -> (rule7 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel does not need the cow.
False
2
inv-proof
[(((triple3) -> rule6))]
("squirrel" "needs" "cow" "-")
((triple3) -> (rule6 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The squirrel visits the cat.
True
3
proof
[(((((triple3) -> rule7)) -> rule4))]
("squirrel" "visits" "cat" "+")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel does not visit the cat.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule4))]
("squirrel" "visits" "cat" "-")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The cat is blue.
True
4
proof
[(((((((triple3) -> rule7)) -> rule4)) -> rule8))]
("cat" "is" "blue" "+")
((((((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The cat is not blue.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule4)) -> rule8))]
("cat" "is" "blue" "-")
((((((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The squirrel does not chase the cat.
Unknown
inv-rconc
[@1: The squirrel chases the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "chases" "cat" "-")
The cat is rough.
Unknown
rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "rough" "+")
The squirrel does not chase the squirrel.
Unknown
inv-rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "chases" "squirrel" "-")
The squirrel is young.
Unknown
rconc
[@2: The squirrel is young.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("squirrel" "is" "young" "+")
The cat does not need the cow.
Unknown
inv-random
[@0: The cat needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cow" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The squirrel chases the cow.
Unknown
random
[@0: The squirrel chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "cow" "+")
@0: The cat is cold.[(triple1)] The cow chases the squirrel.[(triple2)] The squirrel visits the cow.[(triple3)] @1: The squirrel is rough.[(((triple3) -> rule7))] The squirrel needs the cow.[(((triple3) -> rule6))] @2: The squirrel visits the cat.[(((((triple3) -> rule7)) -> rule4))] @3: The cat is blue.[(((((((triple3) -> rule7)) -> rule4)) -> rule8))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple2
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple3
The squirrel is rough.
("squirrel" "is" "rough" "+")
((triple3) -> (rule7 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
((triple3) -> (rule6 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
((((((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3