The cow needs the lion. The cow needs the mouse. The cow visits the mouse. The lion is round. The lion sees the cow. The lion sees the mouse. The mouse sees the cow. If something needs the lion then it is young. If something sees the cow then it needs the lion.
The cow needs the lion.
("cow" "needs" "lion" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The lion is round.
("lion" "is" "round" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If something needs the lion then it is young.
((("something" "needs" "lion" "+")) -> ("something" "is" "young" "+"))
If something sees the cow then it needs the lion.
((("something" "sees" "cow" "+")) -> ("something" "needs" "lion" "+"))
The cow needs the mouse.
True
1
proof
[(triple2)]
("cow" "needs" "mouse" "+")
triple2
The mouse does not see the cow.
False
1
inv-proof
[(triple7)]
("mouse" "sees" "cow" "-")
triple7
The lion needs the lion.
True
2
proof
[(((triple5) -> rule2))]
("lion" "needs" "lion" "+")
((triple5) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion does not need the lion.
False
2
inv-proof
[(((triple5) -> rule2))]
("lion" "needs" "lion" "-")
((triple5) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The mouse is young.
True
3
proof
[(((((triple7) -> rule2)) -> rule1))]
("mouse" "is" "young" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The lion is not young.
False
3
inv-proof
[(((((triple5) -> rule2)) -> rule1))]
("lion" "is" "young" "-")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The cow does not see the lion.
Unknown
inv-random
[@0: The cow sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "lion" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The lion does not need the mouse.
Unknown
inv-random
[@0: The lion needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "mouse" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
The lion is not rough.
Unknown
inv-random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The cow needs the lion.[(triple1)] The cow needs the mouse.[(triple2)] The cow visits the mouse.[(triple3)] The lion is round.[(triple4)] The lion sees the cow.[(triple5)] The lion sees the mouse.[(triple6)] The mouse sees the cow.[(triple7)] @1: The cow is young.[(((triple1) -> rule1))] The lion needs the lion.[(((triple5) -> rule2))] The mouse needs the lion.[(((triple7) -> rule2))] @2: The lion is young.[(((((triple5) -> rule2)) -> rule1))] The mouse is young.[(((((triple7) -> rule2)) -> rule1))]
The cow needs the lion.
("cow" "needs" "lion" "+")
triple1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple2
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
triple4
The lion sees the cow.
("lion" "sees" "cow" "+")
triple5
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple6
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple7
The cow is young.
("cow" "is" "young" "+")
((triple1) -> (rule1 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple5) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
((triple7) -> (rule2 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The lion is young.
("lion" "is" "young" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2