The bear eats the rabbit. The bear is red. The bear is round. The bear sees the rabbit. The cat sees the tiger. The rabbit sees the bear. The tiger eats the bear. The tiger eats the cat. The tiger is green. The tiger is red. The tiger is rough. If something is green and it needs the cat then the cat needs the tiger. If something sees the rabbit then it needs the cat. If something sees the cat then it needs the cat. If the cat needs the bear and the cat needs the rabbit then the cat does not see the bear. If something is rough and green then it sees the rabbit. If something is big then it sees the cat. If something needs the tiger then the tiger is big. If something sees the tiger and it does not need the tiger then it eats the bear.
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is round.
("bear" "is" "round" "+")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
If something is green and it needs the cat then the cat needs the tiger.
((("something" "is" "green" "+") ("something" "needs" "cat" "+")) -> ("cat" "needs" "tiger" "+"))
If something sees the rabbit then it needs the cat.
((("something" "sees" "rabbit" "+")) -> ("something" "needs" "cat" "+"))
If something sees the cat then it needs the cat.
((("something" "sees" "cat" "+")) -> ("something" "needs" "cat" "+"))
If the cat needs the bear and the cat needs the rabbit then the cat does not see the bear.
((("cat" "needs" "bear" "+") ("cat" "needs" "rabbit" "+")) -> ("cat" "sees" "bear" "-"))
If something is rough and green then it sees the rabbit.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "sees" "rabbit" "+"))
If something is big then it sees the cat.
((("something" "is" "big" "+")) -> ("something" "sees" "cat" "+"))
If something needs the tiger then the tiger is big.
((("something" "needs" "tiger" "+")) -> ("tiger" "is" "big" "+"))
If something sees the tiger and it does not need the tiger then it eats the bear.
((("something" "sees" "tiger" "+") ("something" "needs" "tiger" "~")) -> ("something" "eats" "bear" "+"))
The tiger eats the cat.
True
1
proof
[(triple8)]
("tiger" "eats" "cat" "+")
triple8
The bear is not round.
False
1
inv-proof
[(triple3)]
("bear" "is" "round" "-")
triple3
The tiger sees the rabbit.
True
3
proof
[(((triple11 triple9) -> rule5))]
("tiger" "sees" "rabbit" "+")
((triple11 triple9) -> (rule5 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The bear does not need the cat.
False
2
inv-proof
[(((triple4) -> rule2))]
("bear" "needs" "cat" "-")
((triple4) -> (rule2 % int1))
The bear needs the cat.
("bear" "needs" "cat" "+")
int1
The tiger needs the cat.
True
4
proof
[(((((triple11 triple9) -> rule5)) -> rule2))]
("tiger" "needs" "cat" "+")
((((triple11 triple9) -> (rule5 % int2))) -> (rule2 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The tiger does not need the cat.
False
4
inv-proof
[(((((triple11 triple9) -> rule5)) -> rule2))]
("tiger" "needs" "cat" "-")
((((triple11 triple9) -> (rule5 % int2))) -> (rule2 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The cat needs the tiger.
True
6
proof
[(((triple9 ((((triple11 triple9) -> rule5)) -> rule2)) -> rule1))]
("cat" "needs" "tiger" "+")
((triple9 ((((triple11 triple9) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int3
The cat does not need the tiger.
False
6
inv-proof
[(((triple9 ((((triple11 triple9) -> rule5)) -> rule2)) -> rule1))]
("cat" "needs" "tiger" "-")
((triple9 ((((triple11 triple9) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int3
The tiger is big.
True
7
proof
[(((((triple9 ((((triple11 triple9) -> rule5)) -> rule2)) -> rule1)) -> rule7))]
("tiger" "is" "big" "+")
((((triple9 ((((triple11 triple9) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int4
The tiger is not big.
False
7
inv-proof
[(((((triple9 ((((triple11 triple9) -> rule5)) -> rule2)) -> rule1)) -> rule7))]
("tiger" "is" "big" "-")
((((triple9 ((((triple11 triple9) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int4
The tiger sees the cat.
True
8
proof
[(((((((triple9 ((((triple11 triple9) -> rule5)) -> rule2)) -> rule1)) -> rule7)) -> rule6))]
("tiger" "sees" "cat" "+")
((((((triple9 ((((triple11 triple9) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int3
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int4
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int5
The tiger does not see the cat.
False
8
inv-proof
[(((((((triple9 ((((triple11 triple9) -> rule5)) -> rule2)) -> rule1)) -> rule7)) -> rule6))]
("tiger" "sees" "cat" "-")
((((((triple9 ((((triple11 triple9) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int3
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int4
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int5
The rabbit does not see the cat.
Unknown
inv-rconc
[@1: The rabbit sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "sees" "cat" "-")
The rabbit eats the bear.
Unknown
rconc
[@1: The rabbit eats the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "eats" "bear" "+")
The cat does not see the rabbit.
Unknown
inv-rconc
[@1: The cat sees the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "sees" "rabbit" "-")
The bear sees the cat.
Unknown
rconc
[@1: The bear sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "sees" "cat" "+")
The cat does not need the cat.
Unknown
inv-rconc
[@2: The cat needs the cat.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("cat" "needs" "cat" "-")
The cat sees the cat.
Unknown
rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "sees" "cat" "+")
The rabbit does not need the bear.
Unknown
inv-random
[@0: The rabbit needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "bear" "-")
The bear needs the rabbit.
Unknown
random
[@0: The bear needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "rabbit" "+")
The rabbit does not need the tiger.
Unknown
inv-random
[@0: The rabbit needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "tiger" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The bear is green.
Unknown
random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "+")
@0: The bear eats the rabbit.[(triple1)] The bear is red.[(triple2)] The bear is round.[(triple3)] The bear sees the rabbit.[(triple4)] The cat sees the tiger.[(triple5)] The rabbit sees the bear.[(triple6)] The tiger eats the bear.[(triple7)] The tiger eats the cat.[(triple8)] The tiger is green.[(triple9)] The tiger is red.[(triple10)] The tiger is rough.[(triple11)] @1: The bear needs the cat.[(((triple4) -> rule2))] The tiger sees the rabbit.[(((triple11 triple9) -> rule5))] @2: The tiger needs the cat.[(((((triple11 triple9) -> rule5)) -> rule2))] @3: The cat needs the tiger.[(((triple9 ((((triple11 triple9) -> rule5)) -> rule2)) -> rule1))] @4: The tiger is big.[(((((triple9 ((((triple11 triple9) -> rule5)) -> rule2)) -> rule1)) -> rule7))] @5: The tiger sees the cat.[(((((((triple9 ((((triple11 triple9) -> rule5)) -> rule2)) -> rule1)) -> rule7)) -> rule6))]
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple1
The bear is red.
("bear" "is" "red" "+")
triple2
The bear is round.
("bear" "is" "round" "+")
triple3
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple4
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple5
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple6
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple7
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple8
The tiger is green.
("tiger" "is" "green" "+")
triple9
The tiger is red.
("tiger" "is" "red" "+")
triple10
The tiger is rough.
("tiger" "is" "rough" "+")
triple11
The bear needs the cat.
("bear" "needs" "cat" "+")
((triple4) -> (rule2 % int1))
The bear needs the cat.
("bear" "needs" "cat" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
((triple11 triple9) -> (rule5 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
((((triple11 triple9) -> (rule5 % int2))) -> (rule2 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
((triple9 ((((triple11 triple9) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int2
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
((((triple9 ((((triple11 triple9) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int4
The tiger sees the cat.
("tiger" "sees" "cat" "+")
((((((triple9 ((((triple11 triple9) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int3
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int4
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int5