The cow eats the rabbit. The cow is cold. The rabbit visits the cow. If something eats the rabbit and the rabbit eats the cow then the cow visits the rabbit. If the rabbit eats the cow and the cow is red then the rabbit is not green. If something visits the cow and the cow visits the rabbit then the rabbit is blue. If something eats the rabbit then the rabbit eats the cow. If something visits the rabbit and it is not red then it eats the rabbit. If something is blue and it visits the rabbit then it needs the rabbit.
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
The cow is cold.
("cow" "is" "cold" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
If something eats the rabbit and the rabbit eats the cow then the cow visits the rabbit.
((("something" "eats" "rabbit" "+") ("rabbit" "eats" "cow" "+")) -> ("cow" "visits" "rabbit" "+"))
If the rabbit eats the cow and the cow is red then the rabbit is not green.
((("rabbit" "eats" "cow" "+") ("cow" "is" "red" "+")) -> ("rabbit" "is" "green" "-"))
If something visits the cow and the cow visits the rabbit then the rabbit is blue.
((("something" "visits" "cow" "+") ("cow" "visits" "rabbit" "+")) -> ("rabbit" "is" "blue" "+"))
If something eats the rabbit then the rabbit eats the cow.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "eats" "cow" "+"))
If something visits the rabbit and it is not red then it eats the rabbit.
((("something" "visits" "rabbit" "+") ("something" "is" "red" "~")) -> ("something" "eats" "rabbit" "+"))
If something is blue and it visits the rabbit then it needs the rabbit.
((("something" "is" "blue" "+") ("something" "visits" "rabbit" "+")) -> ("something" "needs" "rabbit" "+"))
The cow is cold.
True
1
proof
[(triple2)]
("cow" "is" "cold" "+")
triple2
The rabbit does not visit the cow.
False
1
inv-proof
[(triple3)]
("rabbit" "visits" "cow" "-")
triple3
The rabbit eats the cow.
True
2
proof
[(((triple1) -> rule4))]
("rabbit" "eats" "cow" "+")
((triple1) -> (rule4 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The rabbit does not eat the cow.
False
2
inv-proof
[(((triple1) -> rule4))]
("rabbit" "eats" "cow" "-")
((triple1) -> (rule4 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The cow visits the rabbit.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule1))]
("cow" "visits" "rabbit" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int2
The cow does not visit the rabbit.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule1))]
("cow" "visits" "rabbit" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int2
The rabbit is blue.
True
6
proof
[(((triple3 ((triple1 ((triple1) -> rule4)) -> rule1)) -> rule3))]
("rabbit" "is" "blue" "+")
((triple3 ((triple1 ((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int2
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int3
The rabbit is not blue.
False
6
inv-proof
[(((triple3 ((triple1 ((triple1) -> rule4)) -> rule1)) -> rule3))]
("rabbit" "is" "blue" "-")
((triple3 ((triple1 ((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int2
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int3
The rabbit does not eat the rabbit.
Unknown
inv-rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "eats" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "needs" "rabbit" "+")
The cow does not need the rabbit.
Unknown
inv-rconc
[@1: The cow needs the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "needs" "rabbit" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The cow is not blue.
Unknown
inv-random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
@0: The cow eats the rabbit.[(triple1)] The cow is cold.[(triple2)] The rabbit visits the cow.[(triple3)] @1: The rabbit eats the cow.[(((triple1) -> rule4))] @2: The cow visits the rabbit.[(((triple1 ((triple1) -> rule4)) -> rule1))] @3: The rabbit is blue.[(((triple3 ((triple1 ((triple1) -> rule4)) -> rule1)) -> rule3))]
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple3
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
((triple1) -> (rule4 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple3 ((triple1 ((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int2
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int3