The bear chases the rabbit. The bear chases the tiger. The bear is cold. The bear is red. The bear is round. The bear needs the rabbit. The bear visits the rabbit. The bear visits the tiger. The rabbit chases the bear. The rabbit visits the bear. The tiger chases the rabbit. The tiger is cold. The tiger is rough. The tiger is young. The tiger needs the rabbit. If something visits the tiger then it is cold. If something visits the tiger and it is round then it is cold. If something visits the bear and the bear needs the tiger then it needs the tiger. If something needs the bear and the bear is cold then it needs the tiger. If something visits the tiger and the tiger visits the rabbit then the rabbit visits the tiger. If something needs the rabbit and the rabbit chases the bear then it needs the bear.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is round.
("bear" "is" "round" "+")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
If something visits the tiger then it is cold.
((("something" "visits" "tiger" "+")) -> ("something" "is" "cold" "+"))
If something visits the tiger and it is round then it is cold.
((("something" "visits" "tiger" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If something visits the bear and the bear needs the tiger then it needs the tiger.
((("something" "visits" "bear" "+") ("bear" "needs" "tiger" "+")) -> ("something" "needs" "tiger" "+"))
If something needs the bear and the bear is cold then it needs the tiger.
((("something" "needs" "bear" "+") ("bear" "is" "cold" "+")) -> ("something" "needs" "tiger" "+"))
If something visits the tiger and the tiger visits the rabbit then the rabbit visits the tiger.
((("something" "visits" "tiger" "+") ("tiger" "visits" "rabbit" "+")) -> ("rabbit" "visits" "tiger" "+"))
If something needs the rabbit and the rabbit chases the bear then it needs the bear.
((("something" "needs" "rabbit" "+") ("rabbit" "chases" "bear" "+")) -> ("something" "needs" "bear" "+"))
The bear is round.
True
1
proof
[(triple5)]
("bear" "is" "round" "+")
triple5
The tiger does not need the rabbit.
False
1
inv-proof
[(triple15)]
("tiger" "needs" "rabbit" "-")
triple15
The tiger needs the bear.
True
3
proof
[(((triple15 triple9) -> rule6))]
("tiger" "needs" "bear" "+")
((triple15 triple9) -> (rule6 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The bear does not need the bear.
False
3
inv-proof
[(((triple6 triple9) -> rule6))]
("bear" "needs" "bear" "-")
((triple6 triple9) -> (rule6 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The tiger needs the tiger.
True
5
proof
[(((((triple15 triple9) -> rule6) triple3) -> rule4) OR ((((triple15 triple9) -> rule6) ((triple8) -> rule1)) -> rule4) OR ((((triple15 triple9) -> rule6) ((triple8 triple5) -> rule2)) -> rule4))]
("tiger" "needs" "tiger" "+")
((((triple15 triple9) -> (rule6 % int2)) triple3) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int2
((((triple15 triple9) -> (rule6 % int3)) ((triple8) -> (rule1 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
((((triple15 triple9) -> (rule6 % int3)) ((triple8 triple5) -> (rule2 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
The tiger does not need the tiger.
False
5
inv-proof
[(((((triple15 triple9) -> rule6) triple3) -> rule4) OR ((((triple15 triple9) -> rule6) ((triple8) -> rule1)) -> rule4) OR ((((triple15 triple9) -> rule6) ((triple8 triple5) -> rule2)) -> rule4))]
("tiger" "needs" "tiger" "-")
((((triple15 triple9) -> (rule6 % int2)) triple3) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int2
((((triple15 triple9) -> (rule6 % int3)) ((triple8) -> (rule1 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
((((triple15 triple9) -> (rule6 % int3)) ((triple8 triple5) -> (rule2 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
The rabbit needs the tiger.
True
7
proof
[(((triple10 ((((triple6 triple9) -> rule6) triple3) -> rule4)) -> rule3) OR ((triple10 ((((triple6 triple9) -> rule6) ((triple8) -> rule1)) -> rule4)) -> rule3) OR ((triple10 ((((triple6 triple9) -> rule6) ((triple8 triple5) -> rule2)) -> rule4)) -> rule3))]
("rabbit" "needs" "tiger" "+")
((triple10 ((((triple6 triple9) -> (rule6 % int3)) triple3) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The bear needs the bear.
("bear" "needs" "bear" "+")
int3
((triple10 ((((triple6 triple9) -> (rule6 % int4)) ((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
The bear needs the bear.
("bear" "needs" "bear" "+")
int4
((triple10 ((((triple6 triple9) -> (rule6 % int4)) ((triple8 triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
The bear needs the bear.
("bear" "needs" "bear" "+")
int4
The rabbit does not need the tiger.
False
7
inv-proof
[(((triple10 ((((triple6 triple9) -> rule6) triple3) -> rule4)) -> rule3) OR ((triple10 ((((triple6 triple9) -> rule6) ((triple8) -> rule1)) -> rule4)) -> rule3) OR ((triple10 ((((triple6 triple9) -> rule6) ((triple8 triple5) -> rule2)) -> rule4)) -> rule3))]
("rabbit" "needs" "tiger" "-")
((triple10 ((((triple6 triple9) -> (rule6 % int3)) triple3) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The bear needs the bear.
("bear" "needs" "bear" "+")
int3
((triple10 ((((triple6 triple9) -> (rule6 % int4)) ((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
The bear needs the bear.
("bear" "needs" "bear" "+")
int4
((triple10 ((((triple6 triple9) -> (rule6 % int4)) ((triple8 triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
The bear needs the bear.
("bear" "needs" "bear" "+")
int4
The rabbit does not visit the tiger.
Unknown
inv-rconc
[@1: The rabbit visits the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "visits" "tiger" "-")
The rabbit is cold.
Unknown
rconc
[@2: The rabbit is cold.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("rabbit" "is" "cold" "+")
The rabbit does not need the bear.
Unknown
inv-rconc
[@1: The rabbit needs the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "needs" "bear" "-")
The tiger visits the bear.
Unknown
random
[@0: The tiger visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "bear" "+")
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The bear is not rough.
Unknown
inv-random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
@0: The bear chases the rabbit.[(triple1)] The bear chases the tiger.[(triple2)] The bear is cold.[(triple3 OR ((triple8) -> rule1) OR ((triple8 triple5) -> rule2))] The bear is red.[(triple4)] The bear is round.[(triple5)] The bear needs the rabbit.[(triple6)] The bear visits the rabbit.[(triple7)] The bear visits the tiger.[(triple8)] The rabbit chases the bear.[(triple9)] The rabbit visits the bear.[(triple10)] The tiger chases the rabbit.[(triple11)] The tiger is cold.[(triple12)] The tiger is rough.[(triple13)] The tiger is young.[(triple14)] The tiger needs the rabbit.[(triple15)] @1: The bear needs the bear.[(((triple6 triple9) -> rule6))] The tiger needs the bear.[(((triple15 triple9) -> rule6))] @2: The bear needs the tiger.[(((((triple6 triple9) -> rule6) triple3) -> rule4) OR ((((triple6 triple9) -> rule6) ((triple8) -> rule1)) -> rule4) OR ((((triple6 triple9) -> rule6) ((triple8 triple5) -> rule2)) -> rule4))] The tiger needs the tiger.[(((((triple15 triple9) -> rule6) triple3) -> rule4) OR ((((triple15 triple9) -> rule6) ((triple8) -> rule1)) -> rule4) OR ((((triple15 triple9) -> rule6) ((triple8 triple5) -> rule2)) -> rule4))] @3: The rabbit needs the tiger.[(((triple10 ((((triple6 triple9) -> rule6) triple3) -> rule4)) -> rule3) OR ((triple10 ((((triple6 triple9) -> rule6) ((triple8) -> rule1)) -> rule4)) -> rule3) OR ((triple10 ((((triple6 triple9) -> rule6) ((triple8 triple5) -> rule2)) -> rule4)) -> rule3))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple2
The bear is cold.
("bear" "is" "cold" "+")
triple3
((triple8) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
((triple8 triple5) -> (rule2 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is red.
("bear" "is" "red" "+")
triple4
The bear is round.
("bear" "is" "round" "+")
triple5
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple6
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple7
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple8
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple9
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple10
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple11
The tiger is cold.
("tiger" "is" "cold" "+")
triple12
The tiger is rough.
("tiger" "is" "rough" "+")
triple13
The tiger is young.
("tiger" "is" "young" "+")
triple14
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple15
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple6 triple9) -> (rule6 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
((triple15 triple9) -> (rule6 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
((((triple6 triple9) -> (rule6 % int2)) triple3) -> (rule4 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
((((triple6 triple9) -> (rule6 % int3)) ((triple8) -> (rule1 % int2))) -> (rule4 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear needs the bear.
("bear" "needs" "bear" "+")
int3
((((triple6 triple9) -> (rule6 % int3)) ((triple8 triple5) -> (rule2 % int2))) -> (rule4 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear needs the bear.
("bear" "needs" "bear" "+")
int3
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((((triple15 triple9) -> (rule6 % int2)) triple3) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int2
((((triple15 triple9) -> (rule6 % int3)) ((triple8) -> (rule1 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
((((triple15 triple9) -> (rule6 % int3)) ((triple8 triple5) -> (rule2 % int2))) -> (rule4 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
((triple10 ((((triple6 triple9) -> (rule6 % int3)) triple3) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The bear needs the bear.
("bear" "needs" "bear" "+")
int3
((triple10 ((((triple6 triple9) -> (rule6 % int4)) ((triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
The bear needs the bear.
("bear" "needs" "bear" "+")
int4
((triple10 ((((triple6 triple9) -> (rule6 % int4)) ((triple8 triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
The bear needs the bear.
("bear" "needs" "bear" "+")
int4