The cow chases the mouse. The cow is big. The cow is not nice. The cow does not need the mouse. The cow does not visit the mouse. The mouse chases the cow. The mouse visits the cow. If something visits the mouse and it visits the cow then it is not nice. If something is young then it is not nice. If something chases the cow then it visits the mouse.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is not nice.
("cow" "is" "nice" "-")
The cow does not need the mouse.
("cow" "needs" "mouse" "-")
The cow does not visit the mouse.
("cow" "visits" "mouse" "-")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
If something visits the mouse and it visits the cow then it is not nice.
((("something" "visits" "mouse" "+") ("something" "visits" "cow" "+")) -> ("something" "is" "nice" "-"))
If something is young then it is not nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "-"))
If something chases the cow then it visits the mouse.
((("something" "chases" "cow" "+")) -> ("something" "visits" "mouse" "+"))
The cow is big.
True
1
proof
[(triple2)]
("cow" "is" "big" "+")
triple2
The cow needs the mouse.
False
1
inv-proof
[(triple4)]
("cow" "needs" "mouse" "+")
triple4
The mouse visits the mouse.
True
2
proof
[(((triple6) -> rule3))]
("mouse" "visits" "mouse" "+")
((triple6) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse does not visit the mouse.
False
2
inv-proof
[(((triple6) -> rule3))]
("mouse" "visits" "mouse" "-")
((triple6) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is not nice.
True
4
proof
[(((((triple6) -> rule3) triple7) -> rule1))]
("mouse" "is" "nice" "-")
((((triple6) -> (rule3 % int2)) triple7) -> (rule1 % int1))
The mouse is not nice.
("mouse" "is" "nice" "-")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse is nice.
False
4
inv-proof
[(((((triple6) -> rule3) triple7) -> rule1))]
("mouse" "is" "nice" "+")
((((triple6) -> (rule3 % int2)) triple7) -> (rule1 % int1))
The mouse is not nice.
("mouse" "is" "nice" "-")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
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 mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
@0: The cow chases the mouse.[(triple1)] The cow does not need the mouse.[(triple4)] The cow does not visit the mouse.[(triple5)] The cow is big.[(triple2)] The cow is not nice.[(triple3)] The mouse chases the cow.[(triple6)] The mouse visits the cow.[(triple7)] @1: The mouse visits the mouse.[(((triple6) -> rule3))] @2: The mouse is not nice.[(((((triple6) -> rule3) triple7) -> rule1))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
The cow does not need the mouse.
("cow" "needs" "mouse" "-")
triple4
The cow does not visit the mouse.
("cow" "visits" "mouse" "-")
triple5
The cow is big.
("cow" "is" "big" "+")
triple2
The cow is not nice.
("cow" "is" "nice" "-")
triple3
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple6
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple7
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple6) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is not nice.
("mouse" "is" "nice" "-")
((((triple6) -> (rule3 % int2)) triple7) -> (rule1 % int1))
The mouse is not nice.
("mouse" "is" "nice" "-")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2