The cat is young. The rabbit is rough. The squirrel needs the cat. If something visits the rabbit then it is green. If the rabbit chases the squirrel and the rabbit needs the cat then the rabbit is green. If something needs the cat then the cat visits the rabbit.
The cat is young.
("cat" "is" "young" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
If something visits the rabbit then it is green.
((("something" "visits" "rabbit" "+")) -> ("something" "is" "green" "+"))
If the rabbit chases the squirrel and the rabbit needs the cat then the rabbit is green.
((("rabbit" "chases" "squirrel" "+") ("rabbit" "needs" "cat" "+")) -> ("rabbit" "is" "green" "+"))
If something needs the cat then the cat visits the rabbit.
((("something" "needs" "cat" "+")) -> ("cat" "visits" "rabbit" "+"))
The cat is young.
True
1
proof
[(triple1)]
("cat" "is" "young" "+")
triple1
The rabbit is not rough.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "rough" "-")
triple2
The cat visits the rabbit.
True
2
proof
[(((triple3) -> rule3))]
("cat" "visits" "rabbit" "+")
((triple3) -> (rule3 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat does not visit the rabbit.
False
2
inv-proof
[(((triple3) -> rule3))]
("cat" "visits" "rabbit" "-")
((triple3) -> (rule3 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is green.
True
3
proof
[(((((triple3) -> rule3)) -> rule1))]
("cat" "is" "green" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat is not green.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule1))]
("cat" "is" "green" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The squirrel is not green.
Unknown
inv-rconc
[@1: The squirrel is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "green" "-")
The rabbit is green.
Unknown
rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "green" "+")
The rabbit does not chase the squirrel.
Unknown
inv-random
[@0: The rabbit chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "squirrel" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
The squirrel does not chase the rabbit.
Unknown
inv-random
[@0: The squirrel chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "rabbit" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
@0: The cat is young.[(triple1)] The rabbit is rough.[(triple2)] The squirrel needs the cat.[(triple3)] @1: The cat visits the rabbit.[(((triple3) -> rule3))] @2: The cat is green.[(((((triple3) -> rule3)) -> rule1))]
The cat is young.
("cat" "is" "young" "+")
triple1
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple2
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple3
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
((triple3) -> (rule3 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is green.
("cat" "is" "green" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2