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