The bear needs the cow. The cow chases the lion. The cow is cold. The cow is green. The cow needs the bear. The cow sees the rabbit. The lion sees the rabbit. The rabbit chases the bear. The rabbit chases the cow. The rabbit needs the bear. The rabbit sees the cow. The rabbit sees the lion. All red things are big. If something sees the rabbit then it is red. If the bear chases the lion then the bear is cold. If something is big then it chases the rabbit. If something is cold and it sees the rabbit then the rabbit is big. If something is red and it sees the bear then the bear chases the lion. If the rabbit is big then the rabbit sees the lion. If something chases the cow and the cow chases the rabbit then the cow sees the bear.
The bear needs the cow.
("bear" "needs" "cow" "+")
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
All red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something sees the rabbit then it is red.
((("something" "sees" "rabbit" "+")) -> ("something" "is" "red" "+"))
If the bear chases the lion then the bear is cold.
((("bear" "chases" "lion" "+")) -> ("bear" "is" "cold" "+"))
If something is big then it chases the rabbit.
((("something" "is" "big" "+")) -> ("something" "chases" "rabbit" "+"))
If something is cold and it sees the rabbit then the rabbit is big.
((("something" "is" "cold" "+") ("something" "sees" "rabbit" "+")) -> ("rabbit" "is" "big" "+"))
If something is red and it sees the bear then the bear chases the lion.
((("something" "is" "red" "+") ("something" "sees" "bear" "+")) -> ("bear" "chases" "lion" "+"))
If the rabbit is big then the rabbit sees the lion.
((("rabbit" "is" "big" "+")) -> ("rabbit" "sees" "lion" "+"))
If something chases the cow and the cow chases the rabbit then the cow sees the bear.
((("something" "chases" "cow" "+") ("cow" "chases" "rabbit" "+")) -> ("cow" "sees" "bear" "+"))
The bear needs the cow.
True
1
proof
[(triple1)]
("bear" "needs" "cow" "+")
triple1
The rabbit does not chase the bear.
False
1
inv-proof
[(triple8)]
("rabbit" "chases" "bear" "-")
triple8
The rabbit is big.
True
3
proof
[(((triple3 triple6) -> rule5))]
("rabbit" "is" "big" "+")
((triple3 triple6) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The lion is not red.
False
2
inv-proof
[(((triple7) -> rule2))]
("lion" "is" "red" "-")
((triple7) -> (rule2 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The cow is big.
True
3
proof
[(((((triple6) -> rule2)) -> rule1))]
("cow" "is" "big" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The rabbit does not chase the rabbit.
False
4
inv-proof
[(((((triple3 triple6) -> rule5)) -> rule4))]
("rabbit" "chases" "rabbit" "-")
((((triple3 triple6) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The cow chases the rabbit.
True
4
proof
[(((((((triple6) -> rule2)) -> rule1)) -> rule4))]
("cow" "chases" "rabbit" "+")
((((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow does not chase the rabbit.
False
4
inv-proof
[(((((((triple6) -> rule2)) -> rule1)) -> rule4))]
("cow" "chases" "rabbit" "-")
((((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow sees the bear.
True
6
proof
[(((triple9 ((((((triple6) -> rule2)) -> rule1)) -> rule4)) -> rule8))]
("cow" "sees" "bear" "+")
((triple9 ((((((triple6) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is red.
("cow" "is" "red" "+")
int4
The cow does not see the bear.
False
6
inv-proof
[(((triple9 ((((((triple6) -> rule2)) -> rule1)) -> rule4)) -> rule8))]
("cow" "sees" "bear" "-")
((triple9 ((((((triple6) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is red.
("cow" "is" "red" "+")
int4
The bear chases the lion.
True
9
proof
[(((((triple6) -> rule2) ((triple9 ((((((triple6) -> rule2)) -> rule1)) -> rule4)) -> rule8)) -> rule6))]
("bear" "chases" "lion" "+")
((((triple6) -> (rule2 % int5)) ((triple9 ((((((triple6) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1
The cow sees the bear.
("cow" "sees" "bear" "+")
int2
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
The cow is red.
("cow" "is" "red" "+")
int5
The bear does not chase the lion.
False
9
inv-proof
[(((((triple6) -> rule2) ((triple9 ((((((triple6) -> rule2)) -> rule1)) -> rule4)) -> rule8)) -> rule6))]
("bear" "chases" "lion" "-")
((((triple6) -> (rule2 % int5)) ((triple9 ((((((triple6) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1
The cow sees the bear.
("cow" "sees" "bear" "+")
int2
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
The cow is red.
("cow" "is" "red" "+")
int5
The rabbit is not red.
Unknown
inv-rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "red" "-")
The bear is red.
Unknown
rconc
[@1: The bear is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "red" "+")
The bear does not chase the rabbit.
Unknown
inv-rconc
[@3: The bear chases the rabbit.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule2 <- FAIL)]]
("bear" "chases" "rabbit" "-")
The bear is big.
Unknown
rconc
[@2: The bear is big.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("bear" "is" "big" "+")
The bear does not need the lion.
Unknown
inv-random
[@0: The bear needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "lion" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
The lion is not green.
Unknown
inv-random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
The cow is not nice.
Unknown
inv-random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
The bear does not chase the cow.
Unknown
inv-random
[@0: The bear chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "cow" "-")
The bear needs the rabbit.
Unknown
random
[@0: The bear needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "rabbit" "+")
@0: The bear needs the cow.[(triple1)] The cow chases the lion.[(triple2)] The cow is cold.[(triple3)] The cow is green.[(triple4)] The cow needs the bear.[(triple5)] The cow sees the rabbit.[(triple6)] The lion sees the rabbit.[(triple7)] The rabbit chases the bear.[(triple8)] The rabbit chases the cow.[(triple9)] The rabbit needs the bear.[(triple10)] The rabbit sees the cow.[(triple11)] The rabbit sees the lion.[(triple12 OR ((((triple3 triple6) -> rule5)) -> rule7))] @1: The cow is red.[(((triple6) -> rule2))] The lion is red.[(((triple7) -> rule2))] The rabbit is big.[(((triple3 triple6) -> rule5))] @2: The cow is big.[(((((triple6) -> rule2)) -> rule1))] The lion is big.[(((((triple7) -> rule2)) -> rule1))] The rabbit chases the rabbit.[(((((triple3 triple6) -> rule5)) -> rule4))] @3: The cow chases the rabbit.[(((((((triple6) -> rule2)) -> rule1)) -> rule4))] The lion chases the rabbit.[(((((((triple7) -> rule2)) -> rule1)) -> rule4))] @4: The cow sees the bear.[(((triple9 ((((((triple6) -> rule2)) -> rule1)) -> rule4)) -> rule8))] @5: The bear chases the lion.[(((((triple6) -> rule2) ((triple9 ((((((triple6) -> rule2)) -> rule1)) -> rule4)) -> rule8)) -> rule6))] @6: The bear is cold.[(((((((triple6) -> rule2) ((triple9 ((((((triple6) -> rule2)) -> rule1)) -> rule4)) -> rule8)) -> rule6)) -> rule3))]
The bear needs the cow.
("bear" "needs" "cow" "+")
triple1
The cow chases the lion.
("cow" "chases" "lion" "+")
triple2
The cow is cold.
("cow" "is" "cold" "+")
triple3
The cow is green.
("cow" "is" "green" "+")
triple4
The cow needs the bear.
("cow" "needs" "bear" "+")
triple5
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple6
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple7
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple8
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple9
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple10
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple11
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple12
((((triple3 triple6) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The cow is red.
("cow" "is" "red" "+")
((triple6) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The lion is red.
("lion" "is" "red" "+")
((triple7) -> (rule2 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((triple3 triple6) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The cow is big.
("cow" "is" "big" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The lion is big.
("lion" "is" "big" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((((triple3 triple6) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
((((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
((((((triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The cow sees the bear.
("cow" "sees" "bear" "+")
((triple9 ((((((triple6) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is red.
("cow" "is" "red" "+")
int4
The bear chases the lion.
("bear" "chases" "lion" "+")
((((triple6) -> (rule2 % int5)) ((triple9 ((((((triple6) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1
The cow sees the bear.
("cow" "sees" "bear" "+")
int2
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
The cow is red.
("cow" "is" "red" "+")
int5
The bear is cold.
("bear" "is" "cold" "+")
((((((triple6) -> (rule2 % int6)) ((triple9 ((((((triple6) -> (rule2 % int6))) -> (rule1 % int5))) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear chases the lion.
("bear" "chases" "lion" "+")
int2
The cow sees the bear.
("cow" "sees" "bear" "+")
int3
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int4
The cow is big.
("cow" "is" "big" "+")
int5
The cow is red.
("cow" "is" "red" "+")
int6