The cat is round. The cat likes the squirrel. The lion is rough. The lion needs the cat. The squirrel is round. The squirrel likes the lion. The squirrel needs the cat. If someone likes the cat then the cat likes the squirrel. If someone needs the cat and they do not need the lion then the cat likes the squirrel. If someone is big then they need the squirrel. If someone is kind then they are rough. If someone needs the squirrel then they are big. If someone likes the lion then they are big. If someone likes the cat then they are not cold. If someone needs the squirrel then they visit the squirrel.
The cat is round.
("cat" "is" "round" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
If someone likes the cat then the cat likes the squirrel.
((("someone" "likes" "cat" "+")) -> ("cat" "likes" "squirrel" "+"))
If someone needs the cat and they do not need the lion then the cat likes the squirrel.
((("someone" "needs" "cat" "+") ("someone" "needs" "lion" "~")) -> ("cat" "likes" "squirrel" "+"))
If someone is big then they need the squirrel.
((("someone" "is" "big" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone is kind then they are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone needs the squirrel then they are big.
((("someone" "needs" "squirrel" "+")) -> ("someone" "is" "big" "+"))
If someone likes the lion then they are big.
((("someone" "likes" "lion" "+")) -> ("someone" "is" "big" "+"))
If someone likes the cat then they are not cold.
((("someone" "likes" "cat" "+")) -> ("someone" "is" "cold" "-"))
If someone needs the squirrel then they visit the squirrel.
((("someone" "needs" "squirrel" "+")) -> ("someone" "visits" "squirrel" "+"))
The cat likes the squirrel.
True
1
proof
[(triple2)]
("cat" "likes" "squirrel" "+")
triple2
The cat is not round.
False
1
inv-proof
[(triple1)]
("cat" "is" "round" "-")
triple1
The squirrel is big.
True
2
proof
[(((triple6) -> rule6))]
("squirrel" "is" "big" "+")
((triple6) -> (rule6 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is not big.
False
2
inv-proof
[(((triple6) -> rule6))]
("squirrel" "is" "big" "-")
((triple6) -> (rule6 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel needs the squirrel.
True
3
proof
[(((((triple6) -> rule6)) -> rule3))]
("squirrel" "needs" "squirrel" "+")
((((triple6) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel does not need the squirrel.
False
3
inv-proof
[(((((triple6) -> rule6)) -> rule3))]
("squirrel" "needs" "squirrel" "-")
((((triple6) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel visits the squirrel.
True
4
proof
[(((((((triple6) -> rule6)) -> rule3)) -> rule8))]
("squirrel" "visits" "squirrel" "+")
((((((triple6) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3
The squirrel does not visit the squirrel.
False
4
inv-proof
[(((((((triple6) -> rule6)) -> rule3)) -> rule8))]
("squirrel" "visits" "squirrel" "-")
((((((triple6) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3
The lion does not need the squirrel.
Unknown
inv-rconc
[@2: The lion needs the squirrel.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("lion" "needs" "squirrel" "-")
The lion is big.
Unknown
rconc
[@3: The lion is big.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule6 <- FAIL)]]
("lion" "is" "big" "+")
The cat is not rough.
Unknown
inv-rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "rough" "-")
The cat is big.
Unknown
rconc
[@3: The cat is big.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule6 <- FAIL)]]
("cat" "is" "big" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The cat does not like the lion.
Unknown
inv-random
[@0: The cat likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "lion" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat is round.[(triple1)] The cat likes the squirrel.[(triple2)] The lion is rough.[(triple3)] The lion needs the cat.[(triple4)] The squirrel is round.[(triple5)] The squirrel likes the lion.[(triple6)] The squirrel needs the cat.[(triple7)] @1: The squirrel is big.[(((triple6) -> rule6))] @2: The squirrel needs the squirrel.[(((((triple6) -> rule6)) -> rule3))] @3: The squirrel visits the squirrel.[(((((((triple6) -> rule6)) -> rule3)) -> rule8))]
The cat is round.
("cat" "is" "round" "+")
triple1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple2
The lion is rough.
("lion" "is" "rough" "+")
triple3
The lion needs the cat.
("lion" "needs" "cat" "+")
triple4
The squirrel is round.
("squirrel" "is" "round" "+")
triple5
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple6
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple7
The squirrel is big.
("squirrel" "is" "big" "+")
((triple6) -> (rule6 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((((triple6) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((((((triple6) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3