The dog eats the tiger. The mouse is red. The rabbit is big. The rabbit is nice. The rabbit is round. The tiger is big. The tiger needs the dog. If someone is big then they eat the mouse. If someone likes the tiger then they are blue. If someone eats the tiger and they are round then they need the mouse. If someone is blue then they eat the dog. If someone needs the dog then the dog likes the tiger. If someone likes the dog and the dog is red then they are red. If someone eats the dog then the dog is round.
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The mouse is red.
("mouse" "is" "red" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If someone is big then they eat the mouse.
((("someone" "is" "big" "+")) -> ("someone" "eats" "mouse" "+"))
If someone likes the tiger then they are blue.
((("someone" "likes" "tiger" "+")) -> ("someone" "is" "blue" "+"))
If someone eats the tiger and they are round then they need the mouse.
((("someone" "eats" "tiger" "+") ("someone" "is" "round" "+")) -> ("someone" "needs" "mouse" "+"))
If someone is blue then they eat the dog.
((("someone" "is" "blue" "+")) -> ("someone" "eats" "dog" "+"))
If someone needs the dog then the dog likes the tiger.
((("someone" "needs" "dog" "+")) -> ("dog" "likes" "tiger" "+"))
If someone likes the dog and the dog is red then they are red.
((("someone" "likes" "dog" "+") ("dog" "is" "red" "+")) -> ("someone" "is" "red" "+"))
If someone eats the dog then the dog is round.
((("someone" "eats" "dog" "+")) -> ("dog" "is" "round" "+"))
The rabbit is round.
True
1
proof
[(triple5)]
("rabbit" "is" "round" "+")
triple5
The tiger is not big.
False
1
inv-proof
[(triple6)]
("tiger" "is" "big" "-")
triple6
The tiger eats the mouse.
True
2
proof
[(((triple6) -> rule1))]
("tiger" "eats" "mouse" "+")
((triple6) -> (rule1 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger does not eat the mouse.
False
2
inv-proof
[(((triple6) -> rule1))]
("tiger" "eats" "mouse" "-")
((triple6) -> (rule1 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The dog is blue.
True
3
proof
[(((((triple7) -> rule5)) -> rule2))]
("dog" "is" "blue" "+")
((((triple7) -> (rule5 % int2))) -> (rule2 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int2
The dog is not blue.
False
3
inv-proof
[(((((triple7) -> rule5)) -> rule2))]
("dog" "is" "blue" "-")
((((triple7) -> (rule5 % int2))) -> (rule2 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int2
The dog eats the dog.
True
4
proof
[(((((((triple7) -> rule5)) -> rule2)) -> rule4))]
("dog" "eats" "dog" "+")
((((((triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int3
The dog does not eat the dog.
False
4
inv-proof
[(((((((triple7) -> rule5)) -> rule2)) -> rule4))]
("dog" "eats" "dog" "-")
((((((triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int3
The dog is round.
True
5
proof
[(((((((((triple7) -> rule5)) -> rule2)) -> rule4)) -> rule7))]
("dog" "is" "round" "+")
((((((((triple7) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int4
The dog is not round.
False
5
inv-proof
[(((((((((triple7) -> rule5)) -> rule2)) -> rule4)) -> rule7))]
("dog" "is" "round" "-")
((((((((triple7) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int4
The dog needs the mouse.
True
7
proof
[(((triple1 ((((((((triple7) -> rule5)) -> rule2)) -> rule4)) -> rule7)) -> rule3))]
("dog" "needs" "mouse" "+")
((triple1 ((((((((triple7) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
int3
The dog is blue.
("dog" "is" "blue" "+")
int4
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int5
The dog does not need the mouse.
False
7
inv-proof
[(((triple1 ((((((((triple7) -> rule5)) -> rule2)) -> rule4)) -> rule7)) -> rule3))]
("dog" "needs" "mouse" "-")
((triple1 ((((((((triple7) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
int3
The dog is blue.
("dog" "is" "blue" "+")
int4
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int5
The mouse does not need the mouse.
Unknown
inv-rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The tiger needs the mouse.
Unknown
rconc
[@1: The tiger needs the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "needs" "mouse" "+")
The rabbit is not red.
Unknown
inv-rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "is" "red" "-")
The rabbit needs the mouse.
Unknown
rconc
[@1: The rabbit needs the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "needs" "mouse" "+")
The rabbit does not eat the dog.
Unknown
inv-rconc
[@2: The rabbit eats the dog.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("rabbit" "eats" "dog" "-")
The mouse eats the dog.
Unknown
rconc
[@2: The mouse eats the dog.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("mouse" "eats" "dog" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The mouse eats the tiger.
Unknown
random
[@0: The mouse eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "tiger" "+")
@0: The dog eats the tiger.[(triple1)] The mouse is red.[(triple2)] The rabbit is big.[(triple3)] The rabbit is nice.[(triple4)] The rabbit is round.[(triple5)] The tiger is big.[(triple6)] The tiger needs the dog.[(triple7)] @1: The dog likes the tiger.[(((triple7) -> rule5))] The rabbit eats the mouse.[(((triple3) -> rule1))] The tiger eats the mouse.[(((triple6) -> rule1))] @2: The dog is blue.[(((((triple7) -> rule5)) -> rule2))] @3: The dog eats the dog.[(((((((triple7) -> rule5)) -> rule2)) -> rule4))] @4: The dog is round.[(((((((((triple7) -> rule5)) -> rule2)) -> rule4)) -> rule7))] @5: The dog needs the mouse.[(((triple1 ((((((((triple7) -> rule5)) -> rule2)) -> rule4)) -> rule7)) -> rule3))]
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple1
The mouse is red.
("mouse" "is" "red" "+")
triple2
The rabbit is big.
("rabbit" "is" "big" "+")
triple3
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple4
The rabbit is round.
("rabbit" "is" "round" "+")
triple5
The tiger is big.
("tiger" "is" "big" "+")
triple6
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple7
The dog likes the tiger.
("dog" "likes" "tiger" "+")
((triple7) -> (rule5 % int1))
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
((triple3) -> (rule1 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
((triple6) -> (rule1 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
((((triple7) -> (rule5 % int2))) -> (rule2 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
((((((triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int3
The dog is round.
("dog" "is" "round" "+")
((((((((triple7) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int4
The dog needs the mouse.
("dog" "needs" "mouse" "+")
((triple1 ((((((((triple7) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
int3
The dog is blue.
("dog" "is" "blue" "+")
int4
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int5