The cat is big. The squirrel likes the cat. If something visits the cat and it is big then the cat visits the squirrel. If something sees the squirrel then the squirrel does not like the cat. If something sees the cat then it likes the squirrel. If something is big then it visits the squirrel. If something likes the cat and the cat visits the squirrel then the squirrel visits the cat. If the cat does not see the squirrel then the squirrel does not visit the cat. If something visits the squirrel and the squirrel visits the cat then the cat likes the squirrel. If the squirrel sees the cat then the squirrel is green.
The cat is big.
("cat" "is" "big" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
If something visits the cat and it is big then the cat visits the squirrel.
((("something" "visits" "cat" "+") ("something" "is" "big" "+")) -> ("cat" "visits" "squirrel" "+"))
If something sees the squirrel then the squirrel does not like the cat.
((("something" "sees" "squirrel" "+")) -> ("squirrel" "likes" "cat" "-"))
If something sees the cat then it likes the squirrel.
((("something" "sees" "cat" "+")) -> ("something" "likes" "squirrel" "+"))
If something is big then it visits the squirrel.
((("something" "is" "big" "+")) -> ("something" "visits" "squirrel" "+"))
If something likes the cat and the cat visits the squirrel then the squirrel visits the cat.
((("something" "likes" "cat" "+") ("cat" "visits" "squirrel" "+")) -> ("squirrel" "visits" "cat" "+"))
If the cat does not see the squirrel then the squirrel does not visit the cat.
((("cat" "sees" "squirrel" "~")) -> ("squirrel" "visits" "cat" "-"))
If something visits the squirrel and the squirrel visits the cat then the cat likes the squirrel.
((("something" "visits" "squirrel" "+") ("squirrel" "visits" "cat" "+")) -> ("cat" "likes" "squirrel" "+"))
If the squirrel sees the cat then the squirrel is green.
((("squirrel" "sees" "cat" "+")) -> ("squirrel" "is" "green" "+"))
The squirrel likes the cat.
True
1
proof
[(triple2)]
("squirrel" "likes" "cat" "+")
triple2
The cat is not big.
False
1
inv-proof
[(triple1)]
("cat" "is" "big" "-")
triple1
The cat visits the squirrel.
True
2
proof
[(((triple1) -> rule4))]
("cat" "visits" "squirrel" "+")
((triple1) -> (rule4 % int1))
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int1
The cat does not visit the squirrel.
False
2
inv-proof
[(((triple1) -> rule4))]
("cat" "visits" "squirrel" "-")
((triple1) -> (rule4 % int1))
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int1
The squirrel visits the cat.
True
4
proof
[(((triple2 ((triple1) -> rule4)) -> rule5))]
("squirrel" "visits" "cat" "+")
((triple2 ((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int2
The squirrel does not visit the cat.
False
4
inv-proof
[(((triple2 ((triple1) -> rule4)) -> rule5))]
("squirrel" "visits" "cat" "-")
((triple2 ((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int2
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel likes the squirrel.
Unknown
rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "likes" "squirrel" "+")
The squirrel is not green.
Unknown
inv-rconc
[@1: The squirrel is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "is" "green" "-")
The squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
@0: The cat is big.[(triple1)] The squirrel likes the cat.[(triple2)] @1: The cat visits the squirrel.[(((triple1) -> rule4))] @2: The squirrel visits the cat.[(((triple2 ((triple1) -> rule4)) -> rule5))] @3: The cat likes the squirrel.[(((((triple1) -> rule4) ((triple2 ((triple1) -> rule4)) -> rule5)) -> rule7))]
The cat is big.
("cat" "is" "big" "+")
triple1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple2
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
((triple1) -> (rule4 % int1))
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
((triple2 ((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int2
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
((((triple1) -> (rule4 % int3)) ((triple2 ((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int2
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int3