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