The bear does not chase the rabbit. The bear does not eat the cat. The bear eats the rabbit. The bear likes the cat. The cat chases the rabbit. The cat chases the tiger. The cat is blue. The cat is red. The rabbit chases the cat. The rabbit is round. The tiger likes the cat. If something likes the rabbit and it does not eat the bear then the rabbit chases the bear. If something is blue then it eats the tiger. If something eats the cat and the cat chases the rabbit then the rabbit likes the bear. If the rabbit eats the tiger and the rabbit eats the cat then the rabbit is not round. All blue things are big. If something likes the bear and the bear does not like the cat then the cat is not red. If something is big then it likes the tiger. If something likes the cat and the cat likes the tiger then it is blue. If something chases the tiger then the tiger does not like the bear.
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
The bear does not eat the cat.
("bear" "eats" "cat" "-")
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is red.
("cat" "is" "red" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
If something likes the rabbit and it does not eat the bear then the rabbit chases the bear.
((("something" "likes" "rabbit" "+") ("something" "eats" "bear" "~")) -> ("rabbit" "chases" "bear" "+"))
If something is blue then it eats the tiger.
((("something" "is" "blue" "+")) -> ("something" "eats" "tiger" "+"))
If something eats the cat and the cat chases the rabbit then the rabbit likes the bear.
((("something" "eats" "cat" "+") ("cat" "chases" "rabbit" "+")) -> ("rabbit" "likes" "bear" "+"))
If the rabbit eats the tiger and the rabbit eats the cat then the rabbit is not round.
((("rabbit" "eats" "tiger" "+") ("rabbit" "eats" "cat" "+")) -> ("rabbit" "is" "round" "-"))
All blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something likes the bear and the bear does not like the cat then the cat is not red.
((("something" "likes" "bear" "+") ("bear" "likes" "cat" "~")) -> ("cat" "is" "red" "-"))
If something is big then it likes the tiger.
((("something" "is" "big" "+")) -> ("something" "likes" "tiger" "+"))
If something likes the cat and the cat likes the tiger then it is blue.
((("something" "likes" "cat" "+") ("cat" "likes" "tiger" "+")) -> ("something" "is" "blue" "+"))
If something chases the tiger then the tiger does not like the bear.
((("something" "chases" "tiger" "+")) -> ("tiger" "likes" "bear" "-"))
The cat chases the rabbit.
True
1
proof
[(triple5)]
("cat" "chases" "rabbit" "+")
triple5
The bear does not eat the rabbit.
False
1
inv-proof
[(triple3)]
("bear" "eats" "rabbit" "-")
triple3
The tiger does not like the bear.
True
2
proof
[(((triple6) -> rule9))]
("tiger" "likes" "bear" "-")
((triple6) -> (rule9 % int1))
The tiger does not like the bear.
("tiger" "likes" "bear" "-")
int1
The cat does not eat the tiger.
False
2
inv-proof
[(((triple7) -> rule2))]
("cat" "eats" "tiger" "-")
((triple7) -> (rule2 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The cat likes the tiger.
True
3
proof
[(((((triple7) -> rule5)) -> rule7))]
("cat" "likes" "tiger" "+")
((((triple7) -> (rule5 % int2))) -> (rule7 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat does not like the tiger.
False
3
inv-proof
[(((((triple7) -> rule5)) -> rule7))]
("cat" "likes" "tiger" "-")
((((triple7) -> (rule5 % int2))) -> (rule7 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The bear is blue.
True
5
proof
[(((triple4 ((((triple7) -> rule5)) -> rule7)) -> rule8))]
("bear" "is" "blue" "+")
((triple4 ((((triple7) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int2
The cat is big.
("cat" "is" "big" "+")
int3
The tiger is not blue.
False
5
inv-proof
[(((triple11 ((((triple7) -> rule5)) -> rule7)) -> rule8))]
("tiger" "is" "blue" "-")
((triple11 ((((triple7) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int2
The cat is big.
("cat" "is" "big" "+")
int3
The bear is big.
True
6
proof
[(((((triple4 ((((triple7) -> rule5)) -> rule7)) -> rule8)) -> rule5))]
("bear" "is" "big" "+")
((((triple4 ((((triple7) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int3
The cat is big.
("cat" "is" "big" "+")
int4
The tiger is not big.
False
6
inv-proof
[(((((triple11 ((((triple7) -> rule5)) -> rule7)) -> rule8)) -> rule5))]
("tiger" "is" "big" "-")
((((triple11 ((((triple7) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int3
The cat is big.
("cat" "is" "big" "+")
int4
The tiger likes the tiger.
True
7
proof
[(((((((triple11 ((((triple7) -> rule5)) -> rule7)) -> rule8)) -> rule5)) -> rule7))]
("tiger" "likes" "tiger" "+")
((((((triple11 ((((triple7) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int4
The cat is big.
("cat" "is" "big" "+")
int5
The tiger does not like the tiger.
False
7
inv-proof
[(((((((triple11 ((((triple7) -> rule5)) -> rule7)) -> rule8)) -> rule5)) -> rule7))]
("tiger" "likes" "tiger" "-")
((((((triple11 ((((triple7) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int4
The cat is big.
("cat" "is" "big" "+")
int5
The rabbit does not chase the bear.
Unknown
inv-rconc
[@1: The rabbit chases the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "chases" "bear" "-")
The rabbit likes the tiger.
Unknown
rconc
[@3: The rabbit likes the tiger.[CWA. Example of deepest failure = (rule7 <- rule5 <- rule8 <- FAIL)]]
("rabbit" "likes" "tiger" "+")
The rabbit is not big.
Unknown
inv-rconc
[@2: The rabbit is big.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("rabbit" "is" "big" "-")
The rabbit eats the tiger.
Unknown
rconc
[@2: The rabbit eats the tiger.[CWA. Example of deepest failure = (rule2 <- rule8 <- FAIL)]]
("rabbit" "eats" "tiger" "+")
The rabbit does not like the bear.
Unknown
inv-rconc
[@1: The rabbit likes the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "likes" "bear" "-")
The rabbit is blue.
Unknown
rconc
[@1: The rabbit is blue.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "is" "blue" "+")
The cat does not like the bear.
Unknown
inv-random
[@0: The cat likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "bear" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
The bear does not chase the cat.
Unknown
inv-random
[@0: The bear chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "cat" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
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 cat chases the bear.
Unknown
random
[@0: The cat chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "bear" "+")
@0: The bear does not chase the rabbit.[(triple1)] The bear does not eat the cat.[(triple2)] The bear eats the rabbit.[(triple3)] The bear likes the cat.[(triple4)] The cat chases the rabbit.[(triple5)] The cat chases the tiger.[(triple6)] The cat is blue.[(triple7)] The cat is red.[(triple8)] The rabbit chases the cat.[(triple9)] The rabbit is round.[(triple10)] The tiger likes the cat.[(triple11)] @1: The cat eats the tiger.[(((triple7) -> rule2))] The cat is big.[(((triple7) -> rule5))] The tiger does not like the bear.[(((triple6) -> rule9))] @2: The cat likes the tiger.[(((((triple7) -> rule5)) -> rule7))] @3: The bear is blue.[(((triple4 ((((triple7) -> rule5)) -> rule7)) -> rule8))] The tiger is blue.[(((triple11 ((((triple7) -> rule5)) -> rule7)) -> rule8))] @4: The bear eats the tiger.[(((((triple4 ((((triple7) -> rule5)) -> rule7)) -> rule8)) -> rule2))] The bear is big.[(((((triple4 ((((triple7) -> rule5)) -> rule7)) -> rule8)) -> rule5))] The tiger eats the tiger.[(((((triple11 ((((triple7) -> rule5)) -> rule7)) -> rule8)) -> rule2))] The tiger is big.[(((((triple11 ((((triple7) -> rule5)) -> rule7)) -> rule8)) -> rule5))] @5: The bear likes the tiger.[(((((((triple4 ((((triple7) -> rule5)) -> rule7)) -> rule8)) -> rule5)) -> rule7))] The tiger likes the tiger.[(((((((triple11 ((((triple7) -> rule5)) -> rule7)) -> rule8)) -> rule5)) -> rule7))]
The bear does not chase the rabbit.
("bear" "chases" "rabbit" "-")
triple1
The bear does not eat the cat.
("bear" "eats" "cat" "-")
triple2
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple3
The bear likes the cat.
("bear" "likes" "cat" "+")
triple4
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple5
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple6
The cat is blue.
("cat" "is" "blue" "+")
triple7
The cat is red.
("cat" "is" "red" "+")
triple8
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple9
The rabbit is round.
("rabbit" "is" "round" "+")
triple10
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple11
The cat eats the tiger.
("cat" "eats" "tiger" "+")
((triple7) -> (rule2 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The cat is big.
("cat" "is" "big" "+")
((triple7) -> (rule5 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The tiger does not like the bear.
("tiger" "likes" "bear" "-")
((triple6) -> (rule9 % int1))
The tiger does not like the bear.
("tiger" "likes" "bear" "-")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
((((triple7) -> (rule5 % int2))) -> (rule7 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
((triple4 ((((triple7) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int2
The cat is big.
("cat" "is" "big" "+")
int3
The tiger is blue.
("tiger" "is" "blue" "+")
((triple11 ((((triple7) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int2
The cat is big.
("cat" "is" "big" "+")
int3
The bear eats the tiger.
("bear" "eats" "tiger" "+")
((((triple4 ((((triple7) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int3
The cat is big.
("cat" "is" "big" "+")
int4
The bear is big.
("bear" "is" "big" "+")
((((triple4 ((((triple7) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int3
The cat is big.
("cat" "is" "big" "+")
int4
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((((triple11 ((((triple7) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int3
The cat is big.
("cat" "is" "big" "+")
int4
The tiger is big.
("tiger" "is" "big" "+")
((((triple11 ((((triple7) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int3
The cat is big.
("cat" "is" "big" "+")
int4
The bear likes the tiger.
("bear" "likes" "tiger" "+")
((((((triple4 ((((triple7) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int4
The cat is big.
("cat" "is" "big" "+")
int5
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((((triple11 ((((triple7) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int4
The cat is big.
("cat" "is" "big" "+")
int5