The bear likes the cat. The cat eats the lion. The lion needs the bear. If someone needs the bear then they do not eat the cat. If the cat is young then the cat is not rough. Red people are big. If someone eats the lion then the lion is cold. If someone likes the lion then they eat the lion. If someone is cold then they like the lion. If someone eats the lion then they do not like the cat. If someone is cold and not big then they are not rough.
The bear likes the cat.
("bear" "likes" "cat" "+")
The cat eats the lion.
("cat" "eats" "lion" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
If someone needs the bear then they do not eat the cat.
((("someone" "needs" "bear" "+")) -> ("someone" "eats" "cat" "-"))
If the cat is young then the cat is not rough.
((("cat" "is" "young" "+")) -> ("cat" "is" "rough" "-"))
Red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone eats the lion then the lion is cold.
((("someone" "eats" "lion" "+")) -> ("lion" "is" "cold" "+"))
If someone likes the lion then they eat the lion.
((("someone" "likes" "lion" "+")) -> ("someone" "eats" "lion" "+"))
If someone is cold then they like the lion.
((("someone" "is" "cold" "+")) -> ("someone" "likes" "lion" "+"))
If someone eats the lion then they do not like the cat.
((("someone" "eats" "lion" "+")) -> ("someone" "likes" "cat" "-"))
If someone is cold and not big then they are not rough.
((("someone" "is" "cold" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "rough" "-"))
The lion needs the bear.
True
1
proof
[(triple3)]
("lion" "needs" "bear" "+")
triple3
The cat does not eat the lion.
False
1
inv-proof
[(triple2)]
("cat" "eats" "lion" "-")
triple2
The lion is cold.
True
2
proof
[(((triple2) -> rule4))]
("lion" "is" "cold" "+")
((triple2) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is not cold.
False
2
inv-proof
[(((triple2) -> rule4))]
("lion" "is" "cold" "-")
((triple2) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion likes the lion.
True
3
proof
[(((((triple2) -> rule4)) -> rule6))]
("lion" "likes" "lion" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion does not like the lion.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule6))]
("lion" "likes" "lion" "-")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion eats the lion.
True
4
proof
[(((((((triple2) -> rule4)) -> rule6)) -> rule5))]
("lion" "eats" "lion" "+")
((((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The lion does not eat the lion.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule6)) -> rule5))]
("lion" "eats" "lion" "-")
((((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The cat is not big.
Unknown
inv-rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "big" "-")
The cat likes the lion.
Unknown
rconc
[@1: The cat likes the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "likes" "lion" "+")
The lion is not big.
Unknown
inv-rconc
[@1: The lion is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "big" "-")
The bear eats the lion.
Unknown
rconc
[@2: The bear eats the lion.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("bear" "eats" "lion" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The lion eats the bear.
Unknown
random
[@0: The lion eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "bear" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
@0: The bear likes the cat.[(triple1)] The cat eats the lion.[(triple2)] The lion needs the bear.[(triple3)] @1: The cat does not like the cat.[(((triple2) -> rule7))] The lion does not eat the cat.[(((triple3) -> rule1))] The lion is cold.[(((triple2) -> rule4))] @2: The lion likes the lion.[(((((triple2) -> rule4)) -> rule6))] @3: The lion eats the lion.[(((((((triple2) -> rule4)) -> rule6)) -> rule5))] @4: The lion does not like the cat.[(((((((((triple2) -> rule4)) -> rule6)) -> rule5)) -> rule7))]
The bear likes the cat.
("bear" "likes" "cat" "+")
triple1
The cat eats the lion.
("cat" "eats" "lion" "+")
triple2
The lion needs the bear.
("lion" "needs" "bear" "+")
triple3
The cat does not like the cat.
("cat" "likes" "cat" "-")
((triple2) -> (rule7 % int1))
The cat does not like the cat.
("cat" "likes" "cat" "-")
int1
The lion does not eat the cat.
("lion" "eats" "cat" "-")
((triple3) -> (rule1 % int1))
The lion does not eat the cat.
("lion" "eats" "cat" "-")
int1
The lion is cold.
("lion" "is" "cold" "+")
((triple2) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
((((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The lion does not like the cat.
("lion" "likes" "cat" "-")
((((((((triple2) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The lion does not like the cat.
("lion" "likes" "cat" "-")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The lion is cold.
("lion" "is" "cold" "+")
int4