The cow is not cold. The cow is nice. The cow is young. The cow needs the mouse. The cow sees the mouse. The cow visits the mouse. The mouse is young. The mouse needs the cow. The mouse sees the cow. The mouse does not visit the cow. If something needs the cow then it visits the mouse. If the cow needs the mouse then the mouse needs the cow. If something sees the cow then the cow is round. If something needs the mouse then it needs the cow. If something needs the cow and the cow does not visit the mouse then the mouse visits the cow. If the mouse sees the cow then the mouse does not visit the cow.
The cow is not cold.
("cow" "is" "cold" "-")
The cow is nice.
("cow" "is" "nice" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
If something needs the cow then it visits the mouse.
((("something" "needs" "cow" "+")) -> ("something" "visits" "mouse" "+"))
If the cow needs the mouse then the mouse needs the cow.
((("cow" "needs" "mouse" "+")) -> ("mouse" "needs" "cow" "+"))
If something sees the cow then the cow is round.
((("something" "sees" "cow" "+")) -> ("cow" "is" "round" "+"))
If something needs the mouse then it needs the cow.
((("something" "needs" "mouse" "+")) -> ("something" "needs" "cow" "+"))
If something needs the cow and the cow does not visit the mouse then the mouse visits the cow.
((("something" "needs" "cow" "+") ("cow" "visits" "mouse" "~")) -> ("mouse" "visits" "cow" "+"))
If the mouse sees the cow then the mouse does not visit the cow.
((("mouse" "sees" "cow" "+")) -> ("mouse" "visits" "cow" "-"))
The cow is not cold.
True
1
proof
[(triple1)]
("cow" "is" "cold" "-")
triple1
The cow is cold.
False
1
inv-proof
[(triple1)]
("cow" "is" "cold" "+")
triple1
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The cow is nice.[(triple2)] The cow is not cold.[(triple1)] The cow is young.[(triple3)] The cow needs the mouse.[(triple4)] The cow sees the mouse.[(triple5)] The cow visits the mouse.[(triple6 OR ((((triple4) -> rule4)) -> rule1))] The mouse does not visit the cow.[(triple10 OR ((triple9) -> rule6))] The mouse is young.[(triple7)] The mouse needs the cow.[(triple8 OR ((triple4) -> rule2))] The mouse sees the cow.[(triple9)] @1: The cow is round.[(((triple9) -> rule3))] The cow needs the cow.[(((triple4) -> rule4))] The mouse visits the mouse.[(((triple8) -> rule1) OR ((((triple4) -> rule2)) -> rule1))]
The cow is nice.
("cow" "is" "nice" "+")
triple2
The cow is not cold.
("cow" "is" "cold" "-")
triple1
The cow is young.
("cow" "is" "young" "+")
triple3
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple4
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple5
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple6
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
The cow visits the mouse.
("cow" "visits" "mouse" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
triple10
((triple9) -> (rule6 % int1))
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
int1
The mouse is young.
("mouse" "is" "young" "+")
triple7
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple8
((triple4) -> (rule2 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple9
The cow is round.
("cow" "is" "round" "+")
((triple9) -> (rule3 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple4) -> (rule4 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple8) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int2