The cat chases the squirrel. The cat is green. The squirrel chases the cat. If the squirrel sees the cat then the squirrel visits the cat. If the cat sees the squirrel then the squirrel sees the cat. If something sees the cat then the cat sees the squirrel. If the squirrel sees the cat and the squirrel is green then the squirrel chases the cat. If something is green then it is round. If the cat is green then the cat sees the squirrel.
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The cat is green.
("cat" "is" "green" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
If the squirrel sees the cat then the squirrel visits the cat.
((("squirrel" "sees" "cat" "+")) -> ("squirrel" "visits" "cat" "+"))
If the cat sees the squirrel then the squirrel sees the cat.
((("cat" "sees" "squirrel" "+")) -> ("squirrel" "sees" "cat" "+"))
If something sees the cat then the cat sees the squirrel.
((("something" "sees" "cat" "+")) -> ("cat" "sees" "squirrel" "+"))
If the squirrel sees the cat and the squirrel is green then the squirrel chases the cat.
((("squirrel" "sees" "cat" "+") ("squirrel" "is" "green" "+")) -> ("squirrel" "chases" "cat" "+"))
If something is green then it is round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If the cat is green then the cat sees the squirrel.
((("cat" "is" "green" "+")) -> ("cat" "sees" "squirrel" "+"))
The cat chases the squirrel.
True
1
proof
[(triple1)]
("cat" "chases" "squirrel" "+")
triple1
The cat does not chase the squirrel.
False
1
inv-proof
[(triple1)]
("cat" "chases" "squirrel" "-")
triple1
The cat sees the squirrel.
True
2
proof
[(((triple2) -> rule6))]
("cat" "sees" "squirrel" "+")
((triple2) -> (rule6 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat does not see the squirrel.
False
2
inv-proof
[(((triple2) -> rule6))]
("cat" "sees" "squirrel" "-")
((triple2) -> (rule6 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The squirrel sees the cat.
True
3
proof
[(((((triple2) -> rule6)) -> rule2))]
("squirrel" "sees" "cat" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The squirrel does not see the cat.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule2))]
("squirrel" "sees" "cat" "-")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The squirrel is not round.
Unknown
inv-rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "round" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The squirrel is not kind.
Unknown
inv-random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "-")
The cat visits the squirrel.
Unknown
random
[@0: The cat visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "squirrel" "+")
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The cat chases the squirrel.[(triple1)] The cat is green.[(triple2)] The squirrel chases the cat.[(triple3)] @1: The cat is round.[(((triple2) -> rule5))] The cat sees the squirrel.[(((triple2) -> rule6))] @2: The squirrel sees the cat.[(((((triple2) -> rule6)) -> rule2))] @3: The squirrel visits the cat.[(((((((triple2) -> rule6)) -> rule2)) -> rule1))]
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
((triple2) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
((triple2) -> (rule6 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int3