The bear is blue. The bear likes the cat. The bear visits the cat. The bear does not visit the cow. The bear visits the rabbit. The cat needs the cow. The cow is blue. The rabbit is cold. The rabbit needs the bear. The rabbit needs the cat. If the rabbit is blue and the cow does not like the rabbit then the cow does not like the bear. If the cat needs the bear then the bear needs the cow. If someone likes the bear then they need the cow. If someone needs the bear and they visit the bear then the bear does not need the cat. If someone needs the cat then the cat likes the rabbit. If someone is rough then they need the bear. If someone is cold then they need the bear. If someone likes the cow and they are not big then they are young. If someone needs the cow then they are cold.
The bear is blue.
("bear" "is" "blue" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The bear does not visit the cow.
("bear" "visits" "cow" "-")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cow is blue.
("cow" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If the rabbit is blue and the cow does not like the rabbit then the cow does not like the bear.
((("rabbit" "is" "blue" "+") ("cow" "likes" "rabbit" "~")) -> ("cow" "likes" "bear" "-"))
If the cat needs the bear then the bear needs the cow.
((("cat" "needs" "bear" "+")) -> ("bear" "needs" "cow" "+"))
If someone likes the bear then they need the cow.
((("someone" "likes" "bear" "+")) -> ("someone" "needs" "cow" "+"))
If someone needs the bear and they visit the bear then the bear does not need the cat.
((("someone" "needs" "bear" "+") ("someone" "visits" "bear" "+")) -> ("bear" "needs" "cat" "-"))
If someone needs the cat then the cat likes the rabbit.
((("someone" "needs" "cat" "+")) -> ("cat" "likes" "rabbit" "+"))
If someone is rough then they need the bear.
((("someone" "is" "rough" "+")) -> ("someone" "needs" "bear" "+"))
If someone is cold then they need the bear.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "bear" "+"))
If someone likes the cow and they are not big then they are young.
((("someone" "likes" "cow" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "young" "+"))
If someone needs the cow then they are cold.
((("someone" "needs" "cow" "+")) -> ("someone" "is" "cold" "+"))
The bear does not visit the cow.
True
1
proof
[(triple4)]
("bear" "visits" "cow" "-")
triple4
The bear does not like the cat.
False
1
inv-proof
[(triple2)]
("bear" "likes" "cat" "-")
triple2
The cat likes the rabbit.
True
2
proof
[(((triple10) -> rule5))]
("cat" "likes" "rabbit" "+")
((triple10) -> (rule5 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
The cat is not cold.
False
2
inv-proof
[(((triple6) -> rule9))]
("cat" "is" "cold" "-")
((triple6) -> (rule9 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat needs the bear.
True
3
proof
[(((((triple6) -> rule9)) -> rule7))]
("cat" "needs" "bear" "+")
((((triple6) -> (rule9 % int2))) -> (rule7 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat does not need the bear.
False
3
inv-proof
[(((((triple6) -> rule9)) -> rule7))]
("cat" "needs" "bear" "-")
((((triple6) -> (rule9 % int2))) -> (rule7 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The bear needs the cow.
True
4
proof
[(((((((triple6) -> rule9)) -> rule7)) -> rule2))]
("bear" "needs" "cow" "+")
((((((triple6) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The bear does not need the cow.
False
4
inv-proof
[(((((((triple6) -> rule9)) -> rule7)) -> rule2))]
("bear" "needs" "cow" "-")
((((((triple6) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The bear is cold.
True
5
proof
[(((((((((triple6) -> rule9)) -> rule7)) -> rule2)) -> rule9))]
("bear" "is" "cold" "+")
((((((((triple6) -> (rule9 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
int2
The cat needs the bear.
("cat" "needs" "bear" "+")
int3
The cat is cold.
("cat" "is" "cold" "+")
int4
The bear is not cold.
False
5
inv-proof
[(((((((((triple6) -> rule9)) -> rule7)) -> rule2)) -> rule9))]
("bear" "is" "cold" "-")
((((((((triple6) -> (rule9 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
int2
The cat needs the bear.
("cat" "needs" "bear" "+")
int3
The cat is cold.
("cat" "is" "cold" "+")
int4
The bear needs the bear.
True
6
proof
[(((((((((((triple6) -> rule9)) -> rule7)) -> rule2)) -> rule9)) -> rule7))]
("bear" "needs" "bear" "+")
((((((((((triple6) -> (rule9 % int5))) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear needs the cow.
("bear" "needs" "cow" "+")
int3
The cat needs the bear.
("cat" "needs" "bear" "+")
int4
The cat is cold.
("cat" "is" "cold" "+")
int5
The bear does not need the bear.
False
6
inv-proof
[(((((((((((triple6) -> rule9)) -> rule7)) -> rule2)) -> rule9)) -> rule7))]
("bear" "needs" "bear" "-")
((((((((((triple6) -> (rule9 % int5))) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear needs the cow.
("bear" "needs" "cow" "+")
int3
The cat needs the bear.
("cat" "needs" "bear" "+")
int4
The cat is cold.
("cat" "is" "cold" "+")
int5
The cow is not cold.
Unknown
inv-rconc
[@2: The cow is cold.[CWA. Example of deepest failure = (rule9 <- rule3 <- FAIL)]]
("cow" "is" "cold" "-")
The rabbit is young.
Unknown
rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "is" "young" "+")
The cow does not need the cow.
Unknown
inv-rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "needs" "cow" "-")
The cow needs the bear.
Unknown
rconc
[@3: The cow needs the bear.[CWA. Example of deepest failure = (rule7 <- rule9 <- rule3 <- FAIL)]]
("cow" "needs" "bear" "+")
The bear is not young.
Unknown
inv-rconc
[@1: The bear is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "is" "young" "-")
The cow is young.
Unknown
rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "is" "young" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The cow visits the bear.
Unknown
random
[@0: The cow visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "bear" "+")
The bear does not need the rabbit.
Unknown
inv-random
[@0: The bear needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "rabbit" "-")
The rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
The cow does not like the cat.
Unknown
inv-random
[@0: The cow likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cat" "-")
The rabbit is blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
@0: The bear does not visit the cow.[(triple4)] The bear is blue.[(triple1)] The bear likes the cat.[(triple2)] The bear visits the cat.[(triple3)] The bear visits the rabbit.[(triple5)] The cat needs the cow.[(triple6)] The cow is blue.[(triple7)] The rabbit is cold.[(triple8)] The rabbit needs the bear.[(triple9 OR ((triple8) -> rule7))] The rabbit needs the cat.[(triple10)] @1: The cat is cold.[(((triple6) -> rule9))] The cat likes the rabbit.[(((triple10) -> rule5))] @2: The cat needs the bear.[(((((triple6) -> rule9)) -> rule7))] @3: The bear needs the cow.[(((((((triple6) -> rule9)) -> rule7)) -> rule2))] @4: The bear is cold.[(((((((((triple6) -> rule9)) -> rule7)) -> rule2)) -> rule9))] @5: The bear needs the bear.[(((((((((((triple6) -> rule9)) -> rule7)) -> rule2)) -> rule9)) -> rule7))]
The bear does not visit the cow.
("bear" "visits" "cow" "-")
triple4
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear likes the cat.
("bear" "likes" "cat" "+")
triple2
The bear visits the cat.
("bear" "visits" "cat" "+")
triple3
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple5
The cat needs the cow.
("cat" "needs" "cow" "+")
triple6
The cow is blue.
("cow" "is" "blue" "+")
triple7
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple8
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple9
((triple8) -> (rule7 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple10
The cat is cold.
("cat" "is" "cold" "+")
((triple6) -> (rule9 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
((triple10) -> (rule5 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
((((triple6) -> (rule9 % int2))) -> (rule7 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The bear needs the cow.
("bear" "needs" "cow" "+")
((((((triple6) -> (rule9 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The bear is cold.
("bear" "is" "cold" "+")
((((((((triple6) -> (rule9 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
int2
The cat needs the bear.
("cat" "needs" "bear" "+")
int3
The cat is cold.
("cat" "is" "cold" "+")
int4
The bear needs the bear.
("bear" "needs" "bear" "+")
((((((((((triple6) -> (rule9 % int5))) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear needs the cow.
("bear" "needs" "cow" "+")
int3
The cat needs the bear.
("cat" "needs" "bear" "+")
int4
The cat is cold.
("cat" "is" "cold" "+")
int5