The cat sees the dog. The cat visits the squirrel. The cow is red. The cow visits the cat. The cow visits the dog. The dog eats the cat. The dog sees the cow. The dog visits the squirrel. The squirrel eats the cow. The squirrel is nice. The squirrel visits the dog. If someone visits the cat then they are nice. If someone visits the cow and the cow visits the cat then the cat eats the squirrel. If someone visits the squirrel and the squirrel eats the cat then they see the squirrel. If the squirrel visits the cat then the cat eats the cow. If someone is blue and they eat the cat then they eat the dog. If someone is red and young then they see the dog. If someone sees the cow and they visit the cat then they see the squirrel. If someone is big and they eat the dog then they see the squirrel. If someone eats the cow and the cow is nice then they visit the cat.
The cat sees the dog.
("cat" "sees" "dog" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The cow is red.
("cow" "is" "red" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog eats the cat.
("dog" "eats" "cat" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If someone visits the cat then they are nice.
((("someone" "visits" "cat" "+")) -> ("someone" "is" "nice" "+"))
If someone visits the cow and the cow visits the cat then the cat eats the squirrel.
((("someone" "visits" "cow" "+") ("cow" "visits" "cat" "+")) -> ("cat" "eats" "squirrel" "+"))
If someone visits the squirrel and the squirrel eats the cat then they see the squirrel.
((("someone" "visits" "squirrel" "+") ("squirrel" "eats" "cat" "+")) -> ("someone" "sees" "squirrel" "+"))
If the squirrel visits the cat then the cat eats the cow.
((("squirrel" "visits" "cat" "+")) -> ("cat" "eats" "cow" "+"))
If someone is blue and they eat the cat then they eat the dog.
((("someone" "is" "blue" "+") ("someone" "eats" "cat" "+")) -> ("someone" "eats" "dog" "+"))
If someone is red and young then they see the dog.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "sees" "dog" "+"))
If someone sees the cow and they visit the cat then they see the squirrel.
((("someone" "sees" "cow" "+") ("someone" "visits" "cat" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone is big and they eat the dog then they see the squirrel.
((("someone" "is" "big" "+") ("someone" "eats" "dog" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone eats the cow and the cow is nice then they visit the cat.
((("someone" "eats" "cow" "+") ("cow" "is" "nice" "+")) -> ("someone" "visits" "cat" "+"))
The cat sees the dog.
True
1
proof
[(triple1)]
("cat" "sees" "dog" "+")
triple1
The squirrel is not nice.
False
1
inv-proof
[(triple10 OR ((((triple9 ((triple4) -> rule1)) -> rule9)) -> rule1))]
("squirrel" "is" "nice" "-")
triple10
((((triple9 ((triple4) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The cow is nice.
True
2
proof
[(((triple4) -> rule1))]
("cow" "is" "nice" "+")
((triple4) -> (rule1 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is not nice.
False
2
inv-proof
[(((triple4) -> rule1))]
("cow" "is" "nice" "-")
((triple4) -> (rule1 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The squirrel visits the cat.
True
4
proof
[(((triple9 ((triple4) -> rule1)) -> rule9))]
("squirrel" "visits" "cat" "+")
((triple9 ((triple4) -> (rule1 % int2))) -> (rule9 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The squirrel does not visit the cat.
False
4
inv-proof
[(((triple9 ((triple4) -> rule1)) -> rule9))]
("squirrel" "visits" "cat" "-")
((triple9 ((triple4) -> (rule1 % int2))) -> (rule9 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cat eats the cow.
True
5
proof
[(((((triple9 ((triple4) -> rule1)) -> rule9)) -> rule4))]
("cat" "eats" "cow" "+")
((((triple9 ((triple4) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The cat does not eat the cow.
False
5
inv-proof
[(((((triple9 ((triple4) -> rule1)) -> rule9)) -> rule4))]
("cat" "eats" "cow" "-")
((((triple9 ((triple4) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The cat visits the cat.
True
8
proof
[(((((((triple9 ((triple4) -> rule1)) -> rule9)) -> rule4) ((triple4) -> rule1)) -> rule9))]
("cat" "visits" "cat" "+")
((((((triple9 ((triple4) -> (rule1 % int4))) -> (rule9 % int3))) -> (rule4 % int2)) ((triple4) -> (rule1 % int4))) -> (rule9 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int3
The cow is nice.
("cow" "is" "nice" "+")
int4
The cat does not visit the cat.
False
8
inv-proof
[(((((((triple9 ((triple4) -> rule1)) -> rule9)) -> rule4) ((triple4) -> rule1)) -> rule9))]
("cat" "visits" "cat" "-")
((((((triple9 ((triple4) -> (rule1 % int4))) -> (rule9 % int3))) -> (rule4 % int2)) ((triple4) -> (rule1 % int4))) -> (rule9 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int3
The cow is nice.
("cow" "is" "nice" "+")
int4
The cat is nice.
True
9
proof
[(((((((((triple9 ((triple4) -> rule1)) -> rule9)) -> rule4) ((triple4) -> rule1)) -> rule9)) -> rule1))]
("cat" "is" "nice" "+")
((((((((triple9 ((triple4) -> (rule1 % int5))) -> (rule9 % int4))) -> (rule4 % int3)) ((triple4) -> (rule1 % int5))) -> (rule9 % int2))) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat eats the cow.
("cat" "eats" "cow" "+")
int3
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int4
The cow is nice.
("cow" "is" "nice" "+")
int5
The cat is not nice.
False
9
inv-proof
[(((((((((triple9 ((triple4) -> rule1)) -> rule9)) -> rule4) ((triple4) -> rule1)) -> rule9)) -> rule1))]
("cat" "is" "nice" "-")
((((((((triple9 ((triple4) -> (rule1 % int5))) -> (rule9 % int4))) -> (rule4 % int3)) ((triple4) -> (rule1 % int5))) -> (rule9 % int2))) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat eats the cow.
("cat" "eats" "cow" "+")
int3
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int4
The cow is nice.
("cow" "is" "nice" "+")
int5
The dog does not see the squirrel.
Unknown
inv-rconc
[@2: The dog sees the squirrel.[CWA. Example of deepest failure = (rule7 <- rule9 <- FAIL)]]
("dog" "sees" "squirrel" "-")
The squirrel sees the dog.
Unknown
rconc
[@1: The squirrel sees the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "sees" "dog" "+")
The cat does not see the squirrel.
Unknown
inv-rconc
[@1: The cat sees the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "sees" "squirrel" "-")
The squirrel eats the dog.
Unknown
rconc
[@1: The squirrel eats the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "eats" "dog" "+")
The dog does not eat the dog.
Unknown
inv-rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "eats" "dog" "-")
The dog is nice.
Unknown
rconc
[@2: The dog is nice.[CWA. Example of deepest failure = (rule1 <- rule9 <- FAIL)]]
("dog" "is" "nice" "+")
The cat does not visit the dog.
Unknown
inv-random
[@0: The cat visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "dog" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
The squirrel is not red.
Unknown
inv-random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "-")
The squirrel visits the cow.
Unknown
random
[@0: The squirrel visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "cow" "+")
The cow does not eat the cow.
Unknown
inv-random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "-")
The dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
@0: The cat sees the dog.[(triple1)] The cat visits the squirrel.[(triple2)] The cow is red.[(triple3)] The cow visits the cat.[(triple4)] The cow visits the dog.[(triple5)] The dog eats the cat.[(triple6)] The dog sees the cow.[(triple7)] The dog visits the squirrel.[(triple8)] The squirrel eats the cow.[(triple9)] The squirrel is nice.[(triple10 OR ((((triple9 ((triple4) -> rule1)) -> rule9)) -> rule1))] The squirrel visits the dog.[(triple11)] @1: The cow is nice.[(((triple4) -> rule1))] @2: The squirrel visits the cat.[(((triple9 ((triple4) -> rule1)) -> rule9))] @3: The cat eats the cow.[(((((triple9 ((triple4) -> rule1)) -> rule9)) -> rule4))] @4: The cat visits the cat.[(((((((triple9 ((triple4) -> rule1)) -> rule9)) -> rule4) ((triple4) -> rule1)) -> rule9))] @5: The cat is nice.[(((((((((triple9 ((triple4) -> rule1)) -> rule9)) -> rule4) ((triple4) -> rule1)) -> rule9)) -> rule1))]
The cat sees the dog.
("cat" "sees" "dog" "+")
triple1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple2
The cow is red.
("cow" "is" "red" "+")
triple3
The cow visits the cat.
("cow" "visits" "cat" "+")
triple4
The cow visits the dog.
("cow" "visits" "dog" "+")
triple5
The dog eats the cat.
("dog" "eats" "cat" "+")
triple6
The dog sees the cow.
("dog" "sees" "cow" "+")
triple7
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple8
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple9
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple10
((((triple9 ((triple4) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple11
The cow is nice.
("cow" "is" "nice" "+")
((triple4) -> (rule1 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
((triple9 ((triple4) -> (rule1 % int2))) -> (rule9 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cat eats the cow.
("cat" "eats" "cow" "+")
((((triple9 ((triple4) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
int3
The cat visits the cat.
("cat" "visits" "cat" "+")
((((((triple9 ((triple4) -> (rule1 % int4))) -> (rule9 % int3))) -> (rule4 % int2)) ((triple4) -> (rule1 % int4))) -> (rule9 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int3
The cow is nice.
("cow" "is" "nice" "+")
int4
The cat is nice.
("cat" "is" "nice" "+")
((((((((triple9 ((triple4) -> (rule1 % int5))) -> (rule9 % int4))) -> (rule4 % int3)) ((triple4) -> (rule1 % int5))) -> (rule9 % int2))) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat eats the cow.
("cat" "eats" "cow" "+")
int3
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int4
The cow is nice.
("cow" "is" "nice" "+")
int5