The cat is young. The squirrel chases the cat. If someone chases the cat then they need the squirrel. If someone needs the squirrel and the squirrel chases the cat then they eat the squirrel. If someone is rough and they chase the squirrel then the squirrel is young.
The cat is young.
("cat" "is" "young" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
If someone chases the cat then they need the squirrel.
((("someone" "chases" "cat" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone needs the squirrel and the squirrel chases the cat then they eat the squirrel.
((("someone" "needs" "squirrel" "+") ("squirrel" "chases" "cat" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone is rough and they chase the squirrel then the squirrel is young.
((("someone" "is" "rough" "+") ("someone" "chases" "squirrel" "+")) -> ("squirrel" "is" "young" "+"))
The squirrel chases the cat.
True
1
proof
[(triple2)]
("squirrel" "chases" "cat" "+")
triple2
The squirrel does not chase the cat.
False
1
inv-proof
[(triple2)]
("squirrel" "chases" "cat" "-")
triple2
The squirrel needs the squirrel.
True
2
proof
[(((triple2) -> rule1))]
("squirrel" "needs" "squirrel" "+")
((triple2) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel does not need the squirrel.
False
2
inv-proof
[(((triple2) -> rule1))]
("squirrel" "needs" "squirrel" "-")
((triple2) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel eats the squirrel.
True
4
proof
[(((((triple2) -> rule1) triple2) -> rule2))]
("squirrel" "eats" "squirrel" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The squirrel does not eat the squirrel.
False
4
inv-proof
[(((((triple2) -> rule1) triple2) -> rule2))]
("squirrel" "eats" "squirrel" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The cat does not need the squirrel.
Unknown
inv-rconc
[@1: The cat needs the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "needs" "squirrel" "-")
The squirrel is young.
Unknown
rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "young" "+")
The cat does not eat the squirrel.
Unknown
inv-rconc
[@2: The cat eats the squirrel.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("cat" "eats" "squirrel" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
@0: The cat is young.[(triple1)] The squirrel chases the cat.[(triple2)] @1: The squirrel needs the squirrel.[(((triple2) -> rule1))] @2: The squirrel eats the squirrel.[(((((triple2) -> rule1) triple2) -> rule2))]
The cat is young.
("cat" "is" "young" "+")
triple1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple2
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((triple2) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2