The dog is blue. The dog is cold. The dog needs the tiger. The squirrel is cold. The squirrel visits the tiger. The tiger eats the dog. The tiger eats the squirrel. The tiger is big. The tiger is blue. The tiger is cold. If someone is round then they eat the dog. If someone visits the tiger and the tiger is round then the tiger visits the squirrel. If someone eats the squirrel then they are big. If someone is kind and they visit the tiger then the tiger needs the squirrel. If someone eats the dog and the dog needs the tiger then the tiger eats the squirrel. All big people are round. If the dog visits the tiger and the dog visits the squirrel then the dog needs the squirrel. If someone visits the squirrel then they eat the tiger.
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
If someone is round then they eat the dog.
((("someone" "is" "round" "+")) -> ("someone" "eats" "dog" "+"))
If someone visits the tiger and the tiger is round then the tiger visits the squirrel.
((("someone" "visits" "tiger" "+") ("tiger" "is" "round" "+")) -> ("tiger" "visits" "squirrel" "+"))
If someone eats the squirrel then they are big.
((("someone" "eats" "squirrel" "+")) -> ("someone" "is" "big" "+"))
If someone is kind and they visit the tiger then the tiger needs the squirrel.
((("someone" "is" "kind" "+") ("someone" "visits" "tiger" "+")) -> ("tiger" "needs" "squirrel" "+"))
If someone eats the dog and the dog needs the tiger then the tiger eats the squirrel.
((("someone" "eats" "dog" "+") ("dog" "needs" "tiger" "+")) -> ("tiger" "eats" "squirrel" "+"))
All big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If the dog visits the tiger and the dog visits the squirrel then the dog needs the squirrel.
((("dog" "visits" "tiger" "+") ("dog" "visits" "squirrel" "+")) -> ("dog" "needs" "squirrel" "+"))
If someone visits the squirrel then they eat the tiger.
((("someone" "visits" "squirrel" "+")) -> ("someone" "eats" "tiger" "+"))
The squirrel visits the tiger.
True
1
proof
[(triple5)]
("squirrel" "visits" "tiger" "+")
triple5
The squirrel does not visit the tiger.
False
1
inv-proof
[(triple5)]
("squirrel" "visits" "tiger" "-")
triple5
The tiger is round.
True
2
proof
[(((triple8) -> rule6) OR ((((triple7) -> rule3)) -> rule6) OR ((((((triple6 triple3) -> rule5)) -> rule3)) -> rule6))]
("tiger" "is" "round" "+")
((triple8) -> (rule6 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
((((((triple6 triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int3
The tiger is not round.
False
2
inv-proof
[(((triple8) -> rule6) OR ((((triple7) -> rule3)) -> rule6) OR ((((((triple6 triple3) -> rule5)) -> rule3)) -> rule6))]
("tiger" "is" "round" "-")
((triple8) -> (rule6 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
((((((triple6 triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int3
The tiger visits the squirrel.
True
4
proof
[(((triple5 ((triple8) -> rule6)) -> rule2) OR ((triple5 ((((triple7) -> rule3)) -> rule6)) -> rule2) OR ((triple5 ((((((triple6 triple3) -> rule5)) -> rule3)) -> rule6)) -> rule2))]
("tiger" "visits" "squirrel" "+")
((triple5 ((triple8) -> (rule6 % int2))) -> (rule2 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
((triple5 ((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
((triple5 ((((((triple6 triple3) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int4
The tiger does not visit the squirrel.
False
4
inv-proof
[(((triple5 ((triple8) -> rule6)) -> rule2) OR ((triple5 ((((triple7) -> rule3)) -> rule6)) -> rule2) OR ((triple5 ((((((triple6 triple3) -> rule5)) -> rule3)) -> rule6)) -> rule2))]
("tiger" "visits" "squirrel" "-")
((triple5 ((triple8) -> (rule6 % int2))) -> (rule2 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
((triple5 ((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
((triple5 ((((((triple6 triple3) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int4
The tiger eats the tiger.
True
5
proof
[(((((triple5 ((triple8) -> rule6)) -> rule2)) -> rule8) OR ((((triple5 ((((triple7) -> rule3)) -> rule6)) -> rule2)) -> rule8) OR ((((triple5 ((((((triple6 triple3) -> rule5)) -> rule3)) -> rule6)) -> rule2)) -> rule8))]
("tiger" "eats" "tiger" "+")
((((triple5 ((triple8) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
((((triple5 ((((triple7) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
int4
((((triple5 ((((((triple6 triple3) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
int4
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int5
The tiger does not eat the tiger.
False
5
inv-proof
[(((((triple5 ((triple8) -> rule6)) -> rule2)) -> rule8) OR ((((triple5 ((((triple7) -> rule3)) -> rule6)) -> rule2)) -> rule8) OR ((((triple5 ((((((triple6 triple3) -> rule5)) -> rule3)) -> rule6)) -> rule2)) -> rule8))]
("tiger" "eats" "tiger" "-")
((((triple5 ((triple8) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
((((triple5 ((((triple7) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
int4
((((triple5 ((((((triple6 triple3) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
int4
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int5
The dog does not eat the dog.
Unknown
inv-rconc
[@3: The dog eats the dog.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule3 <- FAIL)]]
("dog" "eats" "dog" "-")
The squirrel eats the dog.
Unknown
rconc
[@3: The squirrel eats the dog.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule3 <- FAIL)]]
("squirrel" "eats" "dog" "+")
The squirrel does not eat the tiger.
Unknown
inv-rconc
[@1: The squirrel eats the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "eats" "tiger" "-")
The dog eats the tiger.
Unknown
rconc
[@1: The dog eats the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "eats" "tiger" "+")
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The squirrel needs the tiger.
Unknown
random
[@0: The squirrel needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "tiger" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
@0: The dog is blue.[(triple1)] The dog is cold.[(triple2)] The dog needs the tiger.[(triple3)] The squirrel is cold.[(triple4)] The squirrel visits the tiger.[(triple5)] The tiger eats the dog.[(triple6 OR ((((triple8) -> rule6)) -> rule1) OR ((((((triple7) -> rule3)) -> rule6)) -> rule1))] The tiger eats the squirrel.[(triple7 OR ((triple6 triple3) -> rule5) OR ((((((triple8) -> rule6)) -> rule1) triple3) -> rule5))] The tiger is big.[(triple8 OR ((triple7) -> rule3) OR ((((triple6 triple3) -> rule5)) -> rule3))] The tiger is blue.[(triple9)] The tiger is cold.[(triple10)] @1: The tiger is round.[(((triple8) -> rule6) OR ((((triple7) -> rule3)) -> rule6) OR ((((((triple6 triple3) -> rule5)) -> rule3)) -> rule6))] @2: The tiger visits the squirrel.[(((triple5 ((triple8) -> rule6)) -> rule2) OR ((triple5 ((((triple7) -> rule3)) -> rule6)) -> rule2) OR ((triple5 ((((((triple6 triple3) -> rule5)) -> rule3)) -> rule6)) -> rule2))] @3: The tiger eats the tiger.[(((((triple5 ((triple8) -> rule6)) -> rule2)) -> rule8) OR ((((triple5 ((((triple7) -> rule3)) -> rule6)) -> rule2)) -> rule8) OR ((((triple5 ((((((triple6 triple3) -> rule5)) -> rule3)) -> rule6)) -> rule2)) -> rule8))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple3
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple4
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple5
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple6
((((triple8) -> (rule6 % int2))) -> (rule1 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
((((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple7
((triple6 triple3) -> (rule5 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
((((((triple8) -> (rule6 % int3))) -> (rule1 % int2)) triple3) -> (rule5 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
triple8
((triple7) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
((((triple6 triple3) -> (rule5 % int2))) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger is cold.
("tiger" "is" "cold" "+")
triple10
The tiger is round.
("tiger" "is" "round" "+")
((triple8) -> (rule6 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule6 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
((((((triple6 triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int3
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
((triple5 ((triple8) -> (rule6 % int2))) -> (rule2 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
((triple5 ((((triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
((triple5 ((((((triple6 triple3) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int4
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((((triple5 ((triple8) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
((((triple5 ((((triple7) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
int4
((((triple5 ((((((triple6 triple3) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
int4
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int5