The cat eats the dog. The dog visits the squirrel. The squirrel visits the dog. If someone visits the squirrel and they are kind then the squirrel eats the dog. If someone visits the dog then the dog visits the cat. If someone eats the squirrel then they visit the dog. If someone eats the dog then they eat the squirrel. If the cat visits the dog then the dog eats the squirrel. If someone eats the squirrel and they are blue then they eat the dog.
The cat eats the dog.
("cat" "eats" "dog" "+")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If someone visits the squirrel and they are kind then the squirrel eats the dog.
((("someone" "visits" "squirrel" "+") ("someone" "is" "kind" "+")) -> ("squirrel" "eats" "dog" "+"))
If someone visits the dog then the dog visits the cat.
((("someone" "visits" "dog" "+")) -> ("dog" "visits" "cat" "+"))
If someone eats the squirrel then they visit the dog.
((("someone" "eats" "squirrel" "+")) -> ("someone" "visits" "dog" "+"))
If someone eats the dog then they eat the squirrel.
((("someone" "eats" "dog" "+")) -> ("someone" "eats" "squirrel" "+"))
If the cat visits the dog then the dog eats the squirrel.
((("cat" "visits" "dog" "+")) -> ("dog" "eats" "squirrel" "+"))
If someone eats the squirrel and they are blue then they eat the dog.
((("someone" "eats" "squirrel" "+") ("someone" "is" "blue" "+")) -> ("someone" "eats" "dog" "+"))
The dog visits the squirrel.
True
1
proof
[(triple2)]
("dog" "visits" "squirrel" "+")
triple2
The squirrel does not visit the dog.
False
1
inv-proof
[(triple3)]
("squirrel" "visits" "dog" "-")
triple3
The dog visits the cat.
True
2
proof
[(((triple3) -> rule2) OR ((((((triple1) -> rule4)) -> rule3)) -> rule2) OR ((((((((((triple1) -> rule4)) -> rule3)) -> rule5)) -> rule3)) -> rule2))]
("dog" "visits" "cat" "+")
((triple3) -> (rule2 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int3
((((((((((triple1) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int3
The cat visits the dog.
("cat" "visits" "dog" "+")
int4
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int5
The dog does not visit the cat.
False
2
inv-proof
[(((triple3) -> rule2) OR ((((((triple1) -> rule4)) -> rule3)) -> rule2) OR ((((((((((triple1) -> rule4)) -> rule3)) -> rule5)) -> rule3)) -> rule2))]
("dog" "visits" "cat" "-")
((triple3) -> (rule2 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int3
((((((((((triple1) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int3
The cat visits the dog.
("cat" "visits" "dog" "+")
int4
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int5
The cat visits the dog.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("cat" "visits" "dog" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The cat does not visit the dog.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("cat" "visits" "dog" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The dog eats the squirrel.
True
4
proof
[(((((((triple1) -> rule4)) -> rule3)) -> rule5))]
("dog" "eats" "squirrel" "+")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int3
The dog does not eat the squirrel.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule3)) -> rule5))]
("dog" "eats" "squirrel" "-")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int3
The dog does not eat the dog.
Unknown
inv-rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "eats" "dog" "-")
The squirrel eats the dog.
Unknown
rconc
[@1: The squirrel eats the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "eats" "dog" "+")
The squirrel does not eat the squirrel.
Unknown
inv-rconc
[@2: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("squirrel" "eats" "squirrel" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The squirrel sees the cat.
Unknown
random
[@0: The squirrel sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "cat" "+")
The cat does not see the squirrel.
Unknown
inv-random
[@0: The cat sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "squirrel" "-")
The dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
@0: The cat eats the dog.[(triple1)] The dog visits the squirrel.[(triple2)] The squirrel visits the dog.[(triple3)] @1: The cat eats the squirrel.[(((triple1) -> rule4))] The dog visits the cat.[(((triple3) -> rule2) OR ((((((triple1) -> rule4)) -> rule3)) -> rule2) OR ((((((((((triple1) -> rule4)) -> rule3)) -> rule5)) -> rule3)) -> rule2))] @2: The cat visits the dog.[(((((triple1) -> rule4)) -> rule3))] @3: The dog eats the squirrel.[(((((((triple1) -> rule4)) -> rule3)) -> rule5))] @4: The dog visits the dog.[(((((((((triple1) -> rule4)) -> rule3)) -> rule5)) -> rule3))]
The cat eats the dog.
("cat" "eats" "dog" "+")
triple1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple2
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple3
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
((triple1) -> (rule4 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
((triple3) -> (rule2 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int3
((((((((((triple1) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int3
The cat visits the dog.
("cat" "visits" "dog" "+")
int4
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int5
The cat visits the dog.
("cat" "visits" "dog" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int3
The dog visits the dog.
("dog" "visits" "dog" "+")
((((((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int4