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