The cow chases the mouse. The cow is blue. The cow is nice. The cow is rough. The cow needs the mouse. The cow visits the mouse. The mouse chases the cow. The mouse is nice. The mouse needs the cow. The mouse visits the cow. If something visits the mouse and the mouse is red then the mouse is green. If something needs the cow then it visits the cow. If something visits the cow then it visits the mouse. If the cow is rough and the cow needs the mouse then the cow chases the mouse. If the cow visits the mouse then the mouse visits the cow. If something is blue then it needs the cow. If something visits the cow then it is green. If something needs the cow and the cow is blue then it needs the mouse.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
If something visits the mouse and the mouse is red then the mouse is green.
((("something" "visits" "mouse" "+") ("mouse" "is" "red" "+")) -> ("mouse" "is" "green" "+"))
If something needs the cow then it visits the cow.
((("something" "needs" "cow" "+")) -> ("something" "visits" "cow" "+"))
If something visits the cow then it visits the mouse.
((("something" "visits" "cow" "+")) -> ("something" "visits" "mouse" "+"))
If the cow is rough and the cow needs the mouse then the cow chases the mouse.
((("cow" "is" "rough" "+") ("cow" "needs" "mouse" "+")) -> ("cow" "chases" "mouse" "+"))
If the cow visits the mouse then the mouse visits the cow.
((("cow" "visits" "mouse" "+")) -> ("mouse" "visits" "cow" "+"))
If something is blue then it needs the cow.
((("something" "is" "blue" "+")) -> ("something" "needs" "cow" "+"))
If something visits the cow then it is green.
((("something" "visits" "cow" "+")) -> ("something" "is" "green" "+"))
If something needs the cow and the cow is blue then it needs the mouse.
((("something" "needs" "cow" "+") ("cow" "is" "blue" "+")) -> ("something" "needs" "mouse" "+"))
The mouse visits the cow.
True
1
proof
[(triple10 OR ((triple6) -> rule5) OR ((triple9) -> rule2) OR ((((((((triple2) -> rule6)) -> rule2)) -> rule3)) -> rule5))]
("mouse" "visits" "cow" "+")
triple10
((triple6) -> (rule5 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
((triple9) -> (rule2 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
((((((((triple2) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow needs the cow.
("cow" "needs" "cow" "+")
int4
The mouse does not visit the cow.
False
1
inv-proof
[(triple10 OR ((triple6) -> rule5) OR ((triple9) -> rule2) OR ((((((((triple2) -> rule6)) -> rule2)) -> rule3)) -> rule5))]
("mouse" "visits" "cow" "-")
triple10
((triple6) -> (rule5 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
((triple9) -> (rule2 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
((((((((triple2) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow needs the cow.
("cow" "needs" "cow" "+")
int4
The mouse is green.
True
2
proof
[(((triple10) -> rule7) OR ((((triple6) -> rule5)) -> rule7) OR ((((triple9) -> rule2)) -> rule7) OR ((((((((((triple2) -> rule6)) -> rule2)) -> rule3)) -> rule5)) -> rule7))]
("mouse" "is" "green" "+")
((triple10) -> (rule7 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule7 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
((((triple9) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
((((((((((triple2) -> (rule6 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int3
The cow visits the cow.
("cow" "visits" "cow" "+")
int4
The cow needs the cow.
("cow" "needs" "cow" "+")
int5
The mouse does not visit the mouse.
False
2
inv-proof
[(((triple10) -> rule3) OR ((((triple6) -> rule5)) -> rule3) OR ((((triple9) -> rule2)) -> rule3) OR ((((((((((triple2) -> rule6)) -> rule2)) -> rule3)) -> rule5)) -> rule3))]
("mouse" "visits" "mouse" "-")
((triple10) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
((((((((((triple2) -> (rule6 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int3
The cow visits the cow.
("cow" "visits" "cow" "+")
int4
The cow needs the cow.
("cow" "needs" "cow" "+")
int5
The cow visits the cow.
True
3
proof
[(((((triple2) -> rule6)) -> rule2))]
("cow" "visits" "cow" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow does not visit the cow.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule2))]
("cow" "visits" "cow" "-")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
@0: The cow chases the mouse.[(triple1 OR ((triple4 triple5) -> rule4) OR ((triple4 ((((triple2) -> rule6) triple2) -> rule8)) -> rule4))] The cow is blue.[(triple2)] The cow is nice.[(triple3)] The cow is rough.[(triple4)] The cow needs the mouse.[(triple5 OR ((((triple2) -> rule6) triple2) -> rule8))] The cow visits the mouse.[(triple6 OR ((((((triple2) -> rule6)) -> rule2)) -> rule3))] The mouse chases the cow.[(triple7)] The mouse is nice.[(triple8)] The mouse needs the cow.[(triple9)] The mouse visits the cow.[(triple10 OR ((triple6) -> rule5) OR ((triple9) -> rule2) OR ((((((((triple2) -> rule6)) -> rule2)) -> rule3)) -> rule5))] @1: The cow needs the cow.[(((triple2) -> rule6))] The mouse is green.[(((triple10) -> rule7) OR ((((triple6) -> rule5)) -> rule7) OR ((((triple9) -> rule2)) -> rule7) OR ((((((((((triple2) -> rule6)) -> rule2)) -> rule3)) -> rule5)) -> rule7))] The mouse needs the mouse.[(((triple9 triple2) -> rule8))] The mouse visits the mouse.[(((triple10) -> rule3) OR ((((triple6) -> rule5)) -> rule3) OR ((((triple9) -> rule2)) -> rule3) OR ((((((((((triple2) -> rule6)) -> rule2)) -> rule3)) -> rule5)) -> rule3))] @2: The cow visits the cow.[(((((triple2) -> rule6)) -> rule2))] @3: The cow is green.[(((((((triple2) -> rule6)) -> rule2)) -> rule7))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
((triple4 triple5) -> (rule4 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
((triple4 ((((triple2) -> (rule6 % int3)) triple2) -> (rule8 % int2))) -> (rule4 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow is rough.
("cow" "is" "rough" "+")
triple4
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple5
((((triple2) -> (rule6 % int2)) triple2) -> (rule8 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple6
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple7
The mouse is nice.
("mouse" "is" "nice" "+")
triple8
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple9
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple10
((triple6) -> (rule5 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
((triple9) -> (rule2 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
((((((((triple2) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow needs the cow.
("cow" "needs" "cow" "+")
int4
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple2) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
((triple10) -> (rule7 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule7 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
((((triple9) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
((((((((((triple2) -> (rule6 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int3
The cow visits the cow.
("cow" "visits" "cow" "+")
int4
The cow needs the cow.
("cow" "needs" "cow" "+")
int5
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple9 triple2) -> (rule8 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple10) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
((((((((((triple2) -> (rule6 % int5))) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int3
The cow visits the cow.
("cow" "visits" "cow" "+")
int4
The cow needs the cow.
("cow" "needs" "cow" "+")
int5
The cow visits the cow.
("cow" "visits" "cow" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow is green.
("cow" "is" "green" "+")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3