The bear is young. The bear sees the cat. The cat chases the squirrel. The cat sees the squirrel. The cat visits the bear. The squirrel is green. The squirrel sees the cat. All big things are red. If something sees the squirrel and the squirrel sees the bear then the squirrel chases the cat. If something is blue then it is big. If the squirrel is blue then the squirrel visits the cat. All green things are blue. If something chases the cat then it sees the squirrel.
The bear is young.
("bear" "is" "young" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
All big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something sees the squirrel and the squirrel sees the bear then the squirrel chases the cat.
((("something" "sees" "squirrel" "+") ("squirrel" "sees" "bear" "+")) -> ("squirrel" "chases" "cat" "+"))
If something is blue then it is big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If the squirrel is blue then the squirrel visits the cat.
((("squirrel" "is" "blue" "+")) -> ("squirrel" "visits" "cat" "+"))
All green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If something chases the cat then it sees the squirrel.
((("something" "chases" "cat" "+")) -> ("something" "sees" "squirrel" "+"))
The squirrel sees the cat.
True
1
proof
[(triple7)]
("squirrel" "sees" "cat" "+")
triple7
The cat does not visit the bear.
False
1
inv-proof
[(triple5)]
("cat" "visits" "bear" "-")
triple5
The squirrel is blue.
True
2
proof
[(((triple6) -> rule5))]
("squirrel" "is" "blue" "+")
((triple6) -> (rule5 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is not blue.
False
2
inv-proof
[(((triple6) -> rule5))]
("squirrel" "is" "blue" "-")
((triple6) -> (rule5 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is big.
True
3
proof
[(((((triple6) -> rule5)) -> rule3))]
("squirrel" "is" "big" "+")
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel does not visit the cat.
False
3
inv-proof
[(((((triple6) -> rule5)) -> rule4))]
("squirrel" "visits" "cat" "-")
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is red.
True
4
proof
[(((((((triple6) -> rule5)) -> rule3)) -> rule1))]
("squirrel" "is" "red" "+")
((((((triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
int3
The squirrel is not red.
False
4
inv-proof
[(((((((triple6) -> rule5)) -> rule3)) -> rule1))]
("squirrel" "is" "red" "-")
((((((triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
int3
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@2: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The squirrel chases the cat.
Unknown
rconc
[@1: The squirrel chases the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "chases" "cat" "+")
The cat is not blue.
Unknown
inv-rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "blue" "-")
The cat is big.
Unknown
rconc
[@2: The cat is big.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("cat" "is" "big" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
The squirrel does not see the bear.
Unknown
inv-random
[@0: The squirrel sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "bear" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
@0: The bear is young.[(triple1)] The bear sees the cat.[(triple2)] The cat chases the squirrel.[(triple3)] The cat sees the squirrel.[(triple4)] The cat visits the bear.[(triple5)] The squirrel is green.[(triple6)] The squirrel sees the cat.[(triple7)] @1: The squirrel is blue.[(((triple6) -> rule5))] @2: The squirrel is big.[(((((triple6) -> rule5)) -> rule3))] The squirrel visits the cat.[(((((triple6) -> rule5)) -> rule4))] @3: The squirrel is red.[(((((((triple6) -> rule5)) -> rule3)) -> rule1))]
The bear is young.
("bear" "is" "young" "+")
triple1
The bear sees the cat.
("bear" "sees" "cat" "+")
triple2
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple3
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple4
The cat visits the bear.
("cat" "visits" "bear" "+")
triple5
The squirrel is green.
("squirrel" "is" "green" "+")
triple6
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple7
The squirrel is blue.
("squirrel" "is" "blue" "+")
((triple6) -> (rule5 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
((((((triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
int3