The cat is big. The cat sees the squirrel. The squirrel needs the cat. If someone needs the cat then they see the cat. If someone eats the cat then they need the squirrel. If someone sees the cat and they need the squirrel then the squirrel needs the cat. If someone sees the cat then the cat sees the squirrel. If the squirrel sees the cat then the cat needs the squirrel. If someone needs the cat and the cat is cold then the cat is blue. If someone sees the cat then they are cold. If someone needs the squirrel then they are green.
The cat is big.
("cat" "is" "big" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
If someone needs the cat then they see the cat.
((("someone" "needs" "cat" "+")) -> ("someone" "sees" "cat" "+"))
If someone eats the cat then they need the squirrel.
((("someone" "eats" "cat" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone sees the cat and they need the squirrel then the squirrel needs the cat.
((("someone" "sees" "cat" "+") ("someone" "needs" "squirrel" "+")) -> ("squirrel" "needs" "cat" "+"))
If someone sees the cat then the cat sees the squirrel.
((("someone" "sees" "cat" "+")) -> ("cat" "sees" "squirrel" "+"))
If the squirrel sees the cat then the cat needs the squirrel.
((("squirrel" "sees" "cat" "+")) -> ("cat" "needs" "squirrel" "+"))
If someone needs the cat and the cat is cold then the cat is blue.
((("someone" "needs" "cat" "+") ("cat" "is" "cold" "+")) -> ("cat" "is" "blue" "+"))
If someone sees the cat then they are cold.
((("someone" "sees" "cat" "+")) -> ("someone" "is" "cold" "+"))
If someone needs the squirrel then they are green.
((("someone" "needs" "squirrel" "+")) -> ("someone" "is" "green" "+"))
The cat is big.
True
1
proof
[(triple1)]
("cat" "is" "big" "+")
triple1
The cat is not big.
False
1
inv-proof
[(triple1)]
("cat" "is" "big" "-")
triple1
The squirrel sees the cat.
True
2
proof
[(((triple3) -> rule1))]
("squirrel" "sees" "cat" "+")
((triple3) -> (rule1 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The squirrel does not see the cat.
False
2
inv-proof
[(((triple3) -> rule1))]
("squirrel" "sees" "cat" "-")
((triple3) -> (rule1 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The cat needs the squirrel.
True
3
proof
[(((((triple3) -> rule1)) -> rule5))]
("cat" "needs" "squirrel" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2
The squirrel is not cold.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule7))]
("squirrel" "is" "cold" "-")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2
The cat is green.
True
4
proof
[(((((((triple3) -> rule1)) -> rule5)) -> rule8))]
("cat" "is" "green" "+")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int2
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int3
The cat is not green.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule5)) -> rule8))]
("cat" "is" "green" "-")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int2
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int3
The cat is not blue.
Unknown
inv-rconc
[@3: The cat is blue.[CWA. Example of deepest failure = (rule6 <- rule7 <- rule1 <- FAIL)]]
("cat" "is" "blue" "-")
The squirrel is green.
Unknown
rconc
[@2: The squirrel is green.[CWA. Example of deepest failure = (rule8 <- rule2 <- FAIL)]]
("squirrel" "is" "green" "+")
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The cat sees the cat.
Unknown
rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "cat" "+")
The cat does not eat the squirrel.
Unknown
inv-random
[@0: The cat eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "squirrel" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The cat is big.[(triple1)] The cat sees the squirrel.[(triple2 OR ((((triple3) -> rule1)) -> rule4))] The squirrel needs the cat.[(triple3)] @1: The squirrel sees the cat.[(((triple3) -> rule1))] @2: The cat needs the squirrel.[(((((triple3) -> rule1)) -> rule5))] The squirrel is cold.[(((((triple3) -> rule1)) -> rule7))] @3: The cat is green.[(((((((triple3) -> rule1)) -> rule5)) -> rule8))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple2
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple3
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
((triple3) -> (rule1 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2
The cat is green.
("cat" "is" "green" "+")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int2
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int3