The rabbit visits the squirrel. The squirrel eats the rabbit. If something is kind and it eats the squirrel then the squirrel chases the rabbit. If something chases the squirrel then it is round. If something is round and it chases the rabbit then the rabbit visits the squirrel. All rough things are round. If something eats the rabbit and the rabbit eats the squirrel then the rabbit visits the squirrel. If the squirrel chases the rabbit then the rabbit eats the squirrel. If the squirrel visits the rabbit then the squirrel is young. If something visits the squirrel then the squirrel chases the rabbit.
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
If something is kind and it eats the squirrel then the squirrel chases the rabbit.
((("something" "is" "kind" "+") ("something" "eats" "squirrel" "+")) -> ("squirrel" "chases" "rabbit" "+"))
If something chases the squirrel then it is round.
((("something" "chases" "squirrel" "+")) -> ("something" "is" "round" "+"))
If something is round and it chases the rabbit then the rabbit visits the squirrel.
((("something" "is" "round" "+") ("something" "chases" "rabbit" "+")) -> ("rabbit" "visits" "squirrel" "+"))
All rough things are round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something eats the rabbit and the rabbit eats the squirrel then the rabbit visits the squirrel.
((("something" "eats" "rabbit" "+") ("rabbit" "eats" "squirrel" "+")) -> ("rabbit" "visits" "squirrel" "+"))
If the squirrel chases the rabbit then the rabbit eats the squirrel.
((("squirrel" "chases" "rabbit" "+")) -> ("rabbit" "eats" "squirrel" "+"))
If the squirrel visits the rabbit then the squirrel is young.
((("squirrel" "visits" "rabbit" "+")) -> ("squirrel" "is" "young" "+"))
If something visits the squirrel then the squirrel chases the rabbit.
((("something" "visits" "squirrel" "+")) -> ("squirrel" "chases" "rabbit" "+"))
The squirrel eats the rabbit.
True
1
proof
[(triple2)]
("squirrel" "eats" "rabbit" "+")
triple2
The squirrel does not eat the rabbit.
False
1
inv-proof
[(triple2)]
("squirrel" "eats" "rabbit" "-")
triple2
The squirrel chases the rabbit.
True
2
proof
[(((triple1) -> rule8))]
("squirrel" "chases" "rabbit" "+")
((triple1) -> (rule8 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
The squirrel does not chase the rabbit.
False
2
inv-proof
[(((triple1) -> rule8))]
("squirrel" "chases" "rabbit" "-")
((triple1) -> (rule8 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
The rabbit eats the squirrel.
True
3
proof
[(((((triple1) -> rule8)) -> rule6))]
("rabbit" "eats" "squirrel" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int2
The rabbit does not eat the squirrel.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule6))]
("rabbit" "eats" "squirrel" "-")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int2
The rabbit is not round.
Unknown
inv-rconc
[@1: The rabbit is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "round" "-")
The squirrel is round.
Unknown
rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "round" "+")
The squirrel is not young.
Unknown
inv-rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "is" "young" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The squirrel does not visit the rabbit.
Unknown
inv-random
[@0: The squirrel visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "rabbit" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The rabbit visits the squirrel.[(triple1)] The squirrel eats the rabbit.[(triple2)] @1: The squirrel chases the rabbit.[(((triple1) -> rule8))] @2: The rabbit eats the squirrel.[(((((triple1) -> rule8)) -> rule6))]
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple2
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
((triple1) -> (rule8 % int1))
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
int2