The bear chases the cat. The bear is round. The cat chases the rabbit. The cat eats the tiger. The cat is big. The rabbit is nice. The tiger eats the bear. The tiger is big. The tiger needs the bear. The tiger needs the cat. If the cat eats the bear then the cat needs the rabbit. If someone is big then they chase the rabbit. All nice people are red. If someone needs the rabbit then they are big. If someone needs the bear and they need the cat then the bear is nice. If someone is red then they need the rabbit. If someone needs the bear and they are cold then the bear is cold. If someone eats the tiger then the tiger needs the bear.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear is round.
("bear" "is" "round" "+")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is big.
("cat" "is" "big" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
If the cat eats the bear then the cat needs the rabbit.
((("cat" "eats" "bear" "+")) -> ("cat" "needs" "rabbit" "+"))
If someone is big then they chase the rabbit.
((("someone" "is" "big" "+")) -> ("someone" "chases" "rabbit" "+"))
All nice people are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If someone needs the rabbit then they are big.
((("someone" "needs" "rabbit" "+")) -> ("someone" "is" "big" "+"))
If someone needs the bear and they need the cat then the bear is nice.
((("someone" "needs" "bear" "+") ("someone" "needs" "cat" "+")) -> ("bear" "is" "nice" "+"))
If someone is red then they need the rabbit.
((("someone" "is" "red" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone needs the bear and they are cold then the bear is cold.
((("someone" "needs" "bear" "+") ("someone" "is" "cold" "+")) -> ("bear" "is" "cold" "+"))
If someone eats the tiger then the tiger needs the bear.
((("someone" "eats" "tiger" "+")) -> ("tiger" "needs" "bear" "+"))
The tiger eats the bear.
True
1
proof
[(triple7)]
("tiger" "eats" "bear" "+")
triple7
The tiger is not big.
False
1
inv-proof
[(triple8)]
("tiger" "is" "big" "-")
triple8
The rabbit is red.
True
2
proof
[(((triple6) -> rule3))]
("rabbit" "is" "red" "+")
((triple6) -> (rule3 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is not red.
False
2
inv-proof
[(((triple6) -> rule3))]
("rabbit" "is" "red" "-")
((triple6) -> (rule3 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The bear is red.
True
4
proof
[(((((triple9 triple10) -> rule5)) -> rule3) OR ((((((triple4) -> rule8) triple10) -> rule5)) -> rule3))]
("bear" "is" "red" "+")
((((triple9 triple10) -> (rule5 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
((((((triple4) -> (rule8 % int3)) triple10) -> (rule5 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
The bear is not red.
False
4
inv-proof
[(((((triple9 triple10) -> rule5)) -> rule3) OR ((((((triple4) -> rule8) triple10) -> rule5)) -> rule3))]
("bear" "is" "red" "-")
((((triple9 triple10) -> (rule5 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
((((((triple4) -> (rule8 % int3)) triple10) -> (rule5 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
The rabbit is big.
True
4
proof
[(((((((triple6) -> rule3)) -> rule6)) -> rule4))]
("rabbit" "is" "big" "+")
((((((triple6) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The rabbit is not big.
False
4
inv-proof
[(((((((triple6) -> rule3)) -> rule6)) -> rule4))]
("rabbit" "is" "big" "-")
((((((triple6) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The rabbit chases the rabbit.
True
5
proof
[(((((((((triple6) -> rule3)) -> rule6)) -> rule4)) -> rule2))]
("rabbit" "chases" "rabbit" "+")
((((((((triple6) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The rabbit is red.
("rabbit" "is" "red" "+")
int4
The bear is not big.
False
6
inv-proof
[(((((((((triple9 triple10) -> rule5)) -> rule3)) -> rule6)) -> rule4) OR ((((((((((triple4) -> rule8) triple10) -> rule5)) -> rule3)) -> rule6)) -> rule4))]
("bear" "is" "big" "-")
((((((((triple9 triple10) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4
((((((((((triple4) -> (rule8 % int5)) triple10) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int5
The bear chases the rabbit.
True
7
proof
[(((((((((((triple9 triple10) -> rule5)) -> rule3)) -> rule6)) -> rule4)) -> rule2) OR ((((((((((((triple4) -> rule8) triple10) -> rule5)) -> rule3)) -> rule6)) -> rule4)) -> rule2))]
("bear" "chases" "rabbit" "+")
((((((((((triple9 triple10) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int3
The bear is red.
("bear" "is" "red" "+")
int4
The bear is nice.
("bear" "is" "nice" "+")
int5
((((((((((((triple4) -> (rule8 % int6)) triple10) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int3
The bear is red.
("bear" "is" "red" "+")
int4
The bear is nice.
("bear" "is" "nice" "+")
int5
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int6
The bear does not chase the rabbit.
False
7
inv-proof
[(((((((((((triple9 triple10) -> rule5)) -> rule3)) -> rule6)) -> rule4)) -> rule2) OR ((((((((((((triple4) -> rule8) triple10) -> rule5)) -> rule3)) -> rule6)) -> rule4)) -> rule2))]
("bear" "chases" "rabbit" "-")
((((((((((triple9 triple10) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int3
The bear is red.
("bear" "is" "red" "+")
int4
The bear is nice.
("bear" "is" "nice" "+")
int5
((((((((((((triple4) -> (rule8 % int6)) triple10) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int3
The bear is red.
("bear" "is" "red" "+")
int4
The bear is nice.
("bear" "is" "nice" "+")
int5
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int6
The tiger is not red.
Unknown
inv-rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "red" "-")
The bear is cold.
Unknown
rconc
[@1: The bear is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "is" "cold" "+")
The tiger does not need the rabbit.
Unknown
inv-rconc
[@2: The tiger needs the rabbit.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("tiger" "needs" "rabbit" "-")
The cat is red.
Unknown
rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "red" "+")
The cat does not need the rabbit.
Unknown
inv-rconc
[@2: The cat needs the rabbit.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("cat" "needs" "rabbit" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
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 rabbit eats the bear.
Unknown
random
[@0: The rabbit eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "bear" "+")
The bear does not eat the rabbit.
Unknown
inv-random
[@0: The bear eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "rabbit" "-")
The bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
The rabbit does not chase the tiger.
Unknown
inv-random
[@0: The rabbit chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "tiger" "-")
The tiger eats the cat.
Unknown
random
[@0: The tiger eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "cat" "+")
@0: The bear chases the cat.[(triple1)] The bear is round.[(triple2)] The cat chases the rabbit.[(triple3 OR ((triple5) -> rule2))] The cat eats the tiger.[(triple4)] The cat is big.[(triple5)] The rabbit is nice.[(triple6)] The tiger eats the bear.[(triple7)] The tiger is big.[(triple8)] The tiger needs the bear.[(triple9 OR ((triple4) -> rule8))] The tiger needs the cat.[(triple10)] @1: The bear is nice.[(((triple9 triple10) -> rule5) OR ((((triple4) -> rule8) triple10) -> rule5))] The rabbit is red.[(((triple6) -> rule3))] The tiger chases the rabbit.[(((triple8) -> rule2))] @2: The bear is red.[(((((triple9 triple10) -> rule5)) -> rule3) OR ((((((triple4) -> rule8) triple10) -> rule5)) -> rule3))] The rabbit needs the rabbit.[(((((triple6) -> rule3)) -> rule6))] @3: The bear needs the rabbit.[(((((((triple9 triple10) -> rule5)) -> rule3)) -> rule6) OR ((((((((triple4) -> rule8) triple10) -> rule5)) -> rule3)) -> rule6))] The rabbit is big.[(((((((triple6) -> rule3)) -> rule6)) -> rule4))] @4: The bear is big.[(((((((((triple9 triple10) -> rule5)) -> rule3)) -> rule6)) -> rule4) OR ((((((((((triple4) -> rule8) triple10) -> rule5)) -> rule3)) -> rule6)) -> rule4))] The rabbit chases the rabbit.[(((((((((triple6) -> rule3)) -> rule6)) -> rule4)) -> rule2))] @5: The bear chases the rabbit.[(((((((((((triple9 triple10) -> rule5)) -> rule3)) -> rule6)) -> rule4)) -> rule2) OR ((((((((((((triple4) -> rule8) triple10) -> rule5)) -> rule3)) -> rule6)) -> rule4)) -> rule2))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The bear is round.
("bear" "is" "round" "+")
triple2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple3
((triple5) -> (rule2 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple4
The cat is big.
("cat" "is" "big" "+")
triple5
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple6
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple7
The tiger is big.
("tiger" "is" "big" "+")
triple8
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple9
((triple4) -> (rule8 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple10
The bear is nice.
("bear" "is" "nice" "+")
((triple9 triple10) -> (rule5 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((((triple4) -> (rule8 % int2)) triple10) -> (rule5 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
((triple6) -> (rule3 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
((triple8) -> (rule2 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The bear is red.
("bear" "is" "red" "+")
((((triple9 triple10) -> (rule5 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
((((((triple4) -> (rule8 % int3)) triple10) -> (rule5 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((((triple6) -> (rule3 % int2))) -> (rule6 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
((((((triple9 triple10) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
((((((((triple4) -> (rule8 % int4)) triple10) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int4
The rabbit is big.
("rabbit" "is" "big" "+")
((((((triple6) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The bear is big.
("bear" "is" "big" "+")
((((((((triple9 triple10) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4
((((((((((triple4) -> (rule8 % int5)) triple10) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int5
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((((((((triple6) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The rabbit is red.
("rabbit" "is" "red" "+")
int4
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
((((((((((triple9 triple10) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int3
The bear is red.
("bear" "is" "red" "+")
int4
The bear is nice.
("bear" "is" "nice" "+")
int5
((((((((((((triple4) -> (rule8 % int6)) triple10) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int3
The bear is red.
("bear" "is" "red" "+")
int4
The bear is nice.
("bear" "is" "nice" "+")
int5
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int6