The rabbit eats the squirrel. The squirrel sees the rabbit. If something eats the squirrel and it visits the squirrel then it eats the rabbit. If something is rough then it eats the rabbit. If something visits the squirrel and it eats the rabbit then it is round. If something eats the squirrel then it visits the squirrel. If something is cold then it is big. If the squirrel visits the rabbit and the rabbit does not visit the squirrel then the squirrel is not round.
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If something eats the squirrel and it visits the squirrel then it eats the rabbit.
((("something" "eats" "squirrel" "+") ("something" "visits" "squirrel" "+")) -> ("something" "eats" "rabbit" "+"))
If something is rough then it eats the rabbit.
((("something" "is" "rough" "+")) -> ("something" "eats" "rabbit" "+"))
If something visits the squirrel and it eats the rabbit then it is round.
((("something" "visits" "squirrel" "+") ("something" "eats" "rabbit" "+")) -> ("something" "is" "round" "+"))
If something eats the squirrel then it visits the squirrel.
((("something" "eats" "squirrel" "+")) -> ("something" "visits" "squirrel" "+"))
If something is cold then it is big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If the squirrel visits the rabbit and the rabbit does not visit the squirrel then the squirrel is not round.
((("squirrel" "visits" "rabbit" "+") ("rabbit" "visits" "squirrel" "~")) -> ("squirrel" "is" "round" "-"))
The rabbit eats the squirrel.
True
1
proof
[(triple1)]
("rabbit" "eats" "squirrel" "+")
triple1
The rabbit does not eat the squirrel.
False
1
inv-proof
[(triple1)]
("rabbit" "eats" "squirrel" "-")
triple1
The rabbit visits the squirrel.
True
2
proof
[(((triple1) -> rule4))]
("rabbit" "visits" "squirrel" "+")
((triple1) -> (rule4 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit does not visit the squirrel.
False
2
inv-proof
[(((triple1) -> rule4))]
("rabbit" "visits" "squirrel" "-")
((triple1) -> (rule4 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit eats the rabbit.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule1))]
("rabbit" "eats" "rabbit" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int2
The rabbit does not eat the rabbit.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule1))]
("rabbit" "eats" "rabbit" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int2
The rabbit is round.
True
7
proof
[(((((triple1) -> rule4) ((triple1 ((triple1) -> rule4)) -> rule1)) -> rule3))]
("rabbit" "is" "round" "+")
((((triple1) -> (rule4 % int3)) ((triple1 ((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int3
The rabbit is not round.
False
7
inv-proof
[(((((triple1) -> rule4) ((triple1 ((triple1) -> rule4)) -> rule1)) -> rule3))]
("rabbit" "is" "round" "-")
((((triple1) -> (rule4 % int3)) ((triple1 ((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int3
The squirrel is not big.
Unknown
inv-rconc
[@1: The squirrel is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "big" "-")
The squirrel eats the rabbit.
Unknown
rconc
[@1: The squirrel eats the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "eats" "rabbit" "+")
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel is round.
Unknown
rconc
[@2: The squirrel is round.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("squirrel" "is" "round" "+")
The squirrel is not cold.
Unknown
inv-random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
@0: The rabbit eats the squirrel.[(triple1)] The squirrel sees the rabbit.[(triple2)] @1: The rabbit visits the squirrel.[(((triple1) -> rule4))] @2: The rabbit eats the rabbit.[(((triple1 ((triple1) -> rule4)) -> rule1))] @3: The rabbit is round.[(((((triple1) -> rule4) ((triple1 ((triple1) -> rule4)) -> rule1)) -> rule3))]
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple2
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
((triple1) -> (rule4 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
((((triple1) -> (rule4 % int3)) ((triple1 ((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int3