The dog eats the rabbit. The dog is nice. The dog is red. The dog sees the rabbit. The dog sees the tiger. The rabbit eats the dog. The rabbit eats the tiger. The rabbit is cold. The rabbit likes the dog. The rabbit sees the dog. The tiger eats the dog. The tiger eats the rabbit. The tiger is big. The tiger is red. The tiger sees the dog. The tiger sees the rabbit. If something eats the dog then the dog sees the tiger. If the tiger sees the dog and the tiger is cold then the dog likes the rabbit. If something likes the tiger then it is cold. If something is nice then it sees the tiger. If something is red then it likes the tiger. If something eats the tiger then it is red.
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is red.
("dog" "is" "red" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If something eats the dog then the dog sees the tiger.
((("something" "eats" "dog" "+")) -> ("dog" "sees" "tiger" "+"))
If the tiger sees the dog and the tiger is cold then the dog likes the rabbit.
((("tiger" "sees" "dog" "+") ("tiger" "is" "cold" "+")) -> ("dog" "likes" "rabbit" "+"))
If something likes the tiger then it is cold.
((("something" "likes" "tiger" "+")) -> ("something" "is" "cold" "+"))
If something is nice then it sees the tiger.
((("something" "is" "nice" "+")) -> ("something" "sees" "tiger" "+"))
If something is red then it likes the tiger.
((("something" "is" "red" "+")) -> ("something" "likes" "tiger" "+"))
If something eats the tiger then it is red.
((("something" "eats" "tiger" "+")) -> ("something" "is" "red" "+"))
The tiger is big.
True
1
proof
[(triple13)]
("tiger" "is" "big" "+")
triple13
The dog is not nice.
False
1
inv-proof
[(triple2)]
("dog" "is" "nice" "-")
triple2
The dog likes the tiger.
True
2
proof
[(((triple3) -> rule5))]
("dog" "likes" "tiger" "+")
((triple3) -> (rule5 % int1))
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int1
The dog does not like the tiger.
False
2
inv-proof
[(((triple3) -> rule5))]
("dog" "likes" "tiger" "-")
((triple3) -> (rule5 % int1))
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int1
The rabbit likes the tiger.
True
3
proof
[(((((triple7) -> rule6)) -> rule5))]
("rabbit" "likes" "tiger" "+")
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit does not like the tiger.
False
3
inv-proof
[(((((triple7) -> rule6)) -> rule5))]
("rabbit" "likes" "tiger" "-")
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The dog likes the rabbit.
True
5
proof
[(((triple15 ((((triple14) -> rule5)) -> rule3)) -> rule2))]
("dog" "likes" "rabbit" "+")
((triple15 ((((triple14) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The dog does not like the rabbit.
False
5
inv-proof
[(((triple15 ((((triple14) -> rule5)) -> rule3)) -> rule2))]
("dog" "likes" "rabbit" "-")
((triple15 ((((triple14) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The rabbit does not see the tiger.
Unknown
inv-rconc
[@1: The rabbit sees the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "sees" "tiger" "-")
The tiger sees the tiger.
Unknown
rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "sees" "tiger" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
The tiger does not like the rabbit.
Unknown
inv-random
[@0: The tiger likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "rabbit" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
@0: The dog eats the rabbit.[(triple1)] The dog is nice.[(triple2)] The dog is red.[(triple3)] The dog sees the rabbit.[(triple4)] The dog sees the tiger.[(triple5 OR ((triple11) -> rule1) OR ((triple2) -> rule4) OR ((triple6) -> rule1))] The rabbit eats the dog.[(triple6)] The rabbit eats the tiger.[(triple7)] The rabbit is cold.[(triple8 OR ((((((triple7) -> rule6)) -> rule5)) -> rule3))] The rabbit likes the dog.[(triple9)] The rabbit sees the dog.[(triple10)] The tiger eats the dog.[(triple11)] The tiger eats the rabbit.[(triple12)] The tiger is big.[(triple13)] The tiger is red.[(triple14)] The tiger sees the dog.[(triple15)] The tiger sees the rabbit.[(triple16)] @1: The dog likes the tiger.[(((triple3) -> rule5))] The rabbit is red.[(((triple7) -> rule6))] The tiger likes the tiger.[(((triple14) -> rule5))] @2: The dog is cold.[(((((triple3) -> rule5)) -> rule3))] The rabbit likes the tiger.[(((((triple7) -> rule6)) -> rule5))] The tiger is cold.[(((((triple14) -> rule5)) -> rule3))] @3: The dog likes the rabbit.[(((triple15 ((((triple14) -> rule5)) -> rule3)) -> rule2))]
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple1
The dog is nice.
("dog" "is" "nice" "+")
triple2
The dog is red.
("dog" "is" "red" "+")
triple3
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple4
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple5
((triple11) -> (rule1 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
((triple2) -> (rule4 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
((triple6) -> (rule1 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple6
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple7
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple8
((((((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple9
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple10
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple11
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple12
The tiger is big.
("tiger" "is" "big" "+")
triple13
The tiger is red.
("tiger" "is" "red" "+")
triple14
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple15
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple16
The dog likes the tiger.
("dog" "likes" "tiger" "+")
((triple3) -> (rule5 % int1))
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
((triple7) -> (rule6 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple14) -> (rule5 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog likes the tiger.
("dog" "likes" "tiger" "+")
int2
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
((((triple14) -> (rule5 % int2))) -> (rule3 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
((triple15 ((((triple14) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3