The dog eats the rabbit. The dog is big. The dog is nice. The dog sees the rabbit. The dog does not see the tiger. The rabbit eats the tiger. The rabbit is nice. The rabbit likes the tiger. The tiger eats the dog. The tiger eats the rabbit. The tiger is nice. The tiger is round. The tiger likes the dog. The tiger likes the rabbit. The tiger does not see the dog. If something likes the dog then it is blue. If the tiger likes the rabbit then the rabbit likes the dog.
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The dog does not see the tiger.
("dog" "sees" "tiger" "-")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
If something likes the dog then it is blue.
((("something" "likes" "dog" "+")) -> ("something" "is" "blue" "+"))
If the tiger likes the rabbit then the rabbit likes the dog.
((("tiger" "likes" "rabbit" "+")) -> ("rabbit" "likes" "dog" "+"))
The tiger is round.
True
1
proof
[(triple12)]
("tiger" "is" "round" "+")
triple12
The tiger does not like the rabbit.
False
1
inv-proof
[(triple14)]
("tiger" "likes" "rabbit" "-")
triple14
The rabbit likes the dog.
True
2
proof
[(((triple14) -> rule2))]
("rabbit" "likes" "dog" "+")
((triple14) -> (rule2 % int1))
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int1
The tiger is not blue.
False
2
inv-proof
[(((triple13) -> rule1))]
("tiger" "is" "blue" "-")
((triple13) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The rabbit is blue.
True
3
proof
[(((((triple14) -> rule2)) -> rule1))]
("rabbit" "is" "blue" "+")
((((triple14) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int2
The rabbit is not blue.
False
3
inv-proof
[(((((triple14) -> rule2)) -> rule1))]
("rabbit" "is" "blue" "-")
((((triple14) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int2
The dog is not blue.
Unknown
inv-rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "blue" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
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 tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
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 rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The dog does not see the tiger.[(triple5)] The dog eats the rabbit.[(triple1)] The dog is big.[(triple2)] The dog is nice.[(triple3)] The dog sees the rabbit.[(triple4)] The rabbit eats the tiger.[(triple6)] The rabbit is nice.[(triple7)] The rabbit likes the tiger.[(triple8)] The tiger does not see the dog.[(triple15)] The tiger eats the dog.[(triple9)] The tiger eats the rabbit.[(triple10)] The tiger is nice.[(triple11)] The tiger is round.[(triple12)] The tiger likes the dog.[(triple13)] The tiger likes the rabbit.[(triple14)] @1: The rabbit likes the dog.[(((triple14) -> rule2))] The tiger is blue.[(((triple13) -> rule1))] @2: The rabbit is blue.[(((((triple14) -> rule2)) -> rule1))]
The dog does not see the tiger.
("dog" "sees" "tiger" "-")
triple5
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The dog is nice.
("dog" "is" "nice" "+")
triple3
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple4
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple6
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple7
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple8
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
triple15
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple9
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple10
The tiger is nice.
("tiger" "is" "nice" "+")
triple11
The tiger is round.
("tiger" "is" "round" "+")
triple12
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple13
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple14
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
((triple14) -> (rule2 % int1))
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
((triple13) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((((triple14) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int2