The bear eats the cow. The bear is big. The bear is rough. The cat is nice. The cow eats the bear. The cow eats the cat. The cow likes the cat. If someone is big and they like the cat then they are cold. If the cow is blue then the cow needs the cat. If someone is nice and they eat the bear then the bear likes the cat. If the cat needs the bear then the bear likes the cat. If someone is blue and they like the cat then the cat eats the cow. If someone likes the cat then the cat needs the bear.
The bear eats the cow.
("bear" "eats" "cow" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is rough.
("bear" "is" "rough" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
If someone is big and they like the cat then they are cold.
((("someone" "is" "big" "+") ("someone" "likes" "cat" "+")) -> ("someone" "is" "cold" "+"))
If the cow is blue then the cow needs the cat.
((("cow" "is" "blue" "+")) -> ("cow" "needs" "cat" "+"))
If someone is nice and they eat the bear then the bear likes the cat.
((("someone" "is" "nice" "+") ("someone" "eats" "bear" "+")) -> ("bear" "likes" "cat" "+"))
If the cat needs the bear then the bear likes the cat.
((("cat" "needs" "bear" "+")) -> ("bear" "likes" "cat" "+"))
If someone is blue and they like the cat then the cat eats the cow.
((("someone" "is" "blue" "+") ("someone" "likes" "cat" "+")) -> ("cat" "eats" "cow" "+"))
If someone likes the cat then the cat needs the bear.
((("someone" "likes" "cat" "+")) -> ("cat" "needs" "bear" "+"))
The cow eats the cat.
True
1
proof
[(triple6)]
("cow" "eats" "cat" "+")
triple6
The bear is not big.
False
1
inv-proof
[(triple2)]
("bear" "is" "big" "-")
triple2
The cat needs the bear.
True
2
proof
[(((triple7) -> rule6))]
("cat" "needs" "bear" "+")
((triple7) -> (rule6 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat does not need the bear.
False
2
inv-proof
[(((triple7) -> rule6))]
("cat" "needs" "bear" "-")
((triple7) -> (rule6 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The bear likes the cat.
True
3
proof
[(((((triple7) -> rule6)) -> rule4))]
("bear" "likes" "cat" "+")
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
int2
The bear does not like the cat.
False
3
inv-proof
[(((((triple7) -> rule6)) -> rule4))]
("bear" "likes" "cat" "-")
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
int2
The bear is cold.
True
5
proof
[(((triple2 ((((triple7) -> rule6)) -> rule4)) -> rule1))]
("bear" "is" "cold" "+")
((triple2 ((((triple7) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The cat needs the bear.
("cat" "needs" "bear" "+")
int3
The bear is not cold.
False
5
inv-proof
[(((triple2 ((((triple7) -> rule6)) -> rule4)) -> rule1))]
("bear" "is" "cold" "-")
((triple2 ((((triple7) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The cat needs the bear.
("cat" "needs" "bear" "+")
int3
The cat is not cold.
Unknown
inv-rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "cold" "-")
The cow needs the cat.
Unknown
rconc
[@1: The cow needs the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "needs" "cat" "+")
The cat does not eat the cow.
Unknown
inv-rconc
[@1: The cat eats the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "eats" "cow" "-")
The cow is cold.
Unknown
rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "cold" "+")
The cow does not eat the cow.
Unknown
inv-random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "-")
The cow needs the bear.
Unknown
random
[@0: The cow needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "bear" "+")
The bear does not need the cow.
Unknown
inv-random
[@0: The bear needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "cow" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The bear eats the cow.[(triple1)] The bear is big.[(triple2)] The bear is rough.[(triple3)] The cat is nice.[(triple4)] The cow eats the bear.[(triple5)] The cow eats the cat.[(triple6)] The cow likes the cat.[(triple7)] @1: The cat needs the bear.[(((triple7) -> rule6))] @2: The bear likes the cat.[(((((triple7) -> rule6)) -> rule4))] @3: The bear is cold.[(((triple2 ((((triple7) -> rule6)) -> rule4)) -> rule1))]
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
The cat is nice.
("cat" "is" "nice" "+")
triple4
The cow eats the bear.
("cow" "eats" "bear" "+")
triple5
The cow eats the cat.
("cow" "eats" "cat" "+")
triple6
The cow likes the cat.
("cow" "likes" "cat" "+")
triple7
The cat needs the bear.
("cat" "needs" "bear" "+")
((triple7) -> (rule6 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
((triple2 ((((triple7) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The cat needs the bear.
("cat" "needs" "bear" "+")
int3