The cat does not visit the cow. The cow chases the cat. The cow is blue. The cow visits the cat. The squirrel is big. The squirrel needs the cat. The squirrel visits the cow. If someone is blue then they visit the squirrel. If someone visits the cat then the cat does not visit the squirrel. If the cow needs the cat then the cow is blue. If someone needs the cow then the cow chases the squirrel. If someone is green then they are big. If someone is nice then they visit the cat. If someone needs the cow and they are big then they do not visit the cat. If someone visits the squirrel then they need the cow.
The cat does not visit the cow.
("cat" "visits" "cow" "-")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
If someone is blue then they visit the squirrel.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone visits the cat then the cat does not visit the squirrel.
((("someone" "visits" "cat" "+")) -> ("cat" "visits" "squirrel" "-"))
If the cow needs the cat then the cow is blue.
((("cow" "needs" "cat" "+")) -> ("cow" "is" "blue" "+"))
If someone needs the cow then the cow chases the squirrel.
((("someone" "needs" "cow" "+")) -> ("cow" "chases" "squirrel" "+"))
If someone is green then they are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone is nice then they visit the cat.
((("someone" "is" "nice" "+")) -> ("someone" "visits" "cat" "+"))
If someone needs the cow and they are big then they do not visit the cat.
((("someone" "needs" "cow" "+") ("someone" "is" "big" "+")) -> ("someone" "visits" "cat" "-"))
If someone visits the squirrel then they need the cow.
((("someone" "visits" "squirrel" "+")) -> ("someone" "needs" "cow" "+"))
The squirrel needs the cat.
True
1
proof
[(triple6)]
("squirrel" "needs" "cat" "+")
triple6
The cow does not visit the cat.
False
1
inv-proof
[(triple4)]
("cow" "visits" "cat" "-")
triple4
The cow visits the squirrel.
True
2
proof
[(((triple3) -> rule1))]
("cow" "visits" "squirrel" "+")
((triple3) -> (rule1 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The cow does not visit the squirrel.
False
2
inv-proof
[(((triple3) -> rule1))]
("cow" "visits" "squirrel" "-")
((triple3) -> (rule1 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The cow needs the cow.
True
3
proof
[(((((triple3) -> rule1)) -> rule8))]
("cow" "needs" "cow" "+")
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2
The cow does not need the cow.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule8))]
("cow" "needs" "cow" "-")
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2
The cow chases the squirrel.
True
4
proof
[(((((((triple3) -> rule1)) -> rule8)) -> rule4))]
("cow" "chases" "squirrel" "+")
((((((triple3) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int3
The cow does not chase the squirrel.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule8)) -> rule4))]
("cow" "chases" "squirrel" "-")
((((((triple3) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int3
The cow is not big.
Unknown
inv-rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "big" "-")
The cat needs the cow.
Unknown
rconc
[@1: The cat needs the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "needs" "cow" "+")
The cat does not visit the cat.
Unknown
inv-rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "visits" "cat" "-")
The cat is big.
Unknown
rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "big" "+")
The squirrel is not round.
Unknown
inv-random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
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 cat chases the cow.
Unknown
random
[@0: The cat chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cow" "+")
@0: The cat does not visit the cow.[(triple1)] The cow chases the cat.[(triple2)] The cow is blue.[(triple3)] The cow visits the cat.[(triple4)] The squirrel is big.[(triple5)] The squirrel needs the cat.[(triple6)] The squirrel visits the cow.[(triple7)] @1: The cat does not visit the squirrel.[(((triple4) -> rule2))] The cow visits the squirrel.[(((triple3) -> rule1))] @2: The cow needs the cow.[(((((triple3) -> rule1)) -> rule8))] @3: The cow chases the squirrel.[(((((((triple3) -> rule1)) -> rule8)) -> rule4))]
The cat does not visit the cow.
("cat" "visits" "cow" "-")
triple1
The cow chases the cat.
("cow" "chases" "cat" "+")
triple2
The cow is blue.
("cow" "is" "blue" "+")
triple3
The cow visits the cat.
("cow" "visits" "cat" "+")
triple4
The squirrel is big.
("squirrel" "is" "big" "+")
triple5
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple6
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple7
The cat does not visit the squirrel.
("cat" "visits" "squirrel" "-")
((triple4) -> (rule2 % int1))
The cat does not visit the squirrel.
("cat" "visits" "squirrel" "-")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
((triple3) -> (rule1 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
((((((triple3) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int3