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