The cat eats the cow. The cow is cold. The mouse sees the cow. The squirrel is big. If something eats the cow and it is green then it sees the cow. If something sees the cow then it eats the mouse. If something is big then it sees the cow.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cow is cold.
("cow" "is" "cold" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
If something eats the cow and it is green then it sees the cow.
((("something" "eats" "cow" "+") ("something" "is" "green" "+")) -> ("something" "sees" "cow" "+"))
If something sees the cow then it eats the mouse.
((("something" "sees" "cow" "+")) -> ("something" "eats" "mouse" "+"))
If something is big then it sees the cow.
((("something" "is" "big" "+")) -> ("something" "sees" "cow" "+"))
The squirrel is big.
True
1
proof
[(triple4)]
("squirrel" "is" "big" "+")
triple4
The mouse does not see the cow.
False
1
inv-proof
[(triple3)]
("mouse" "sees" "cow" "-")
triple3
The mouse eats the mouse.
True
2
proof
[(((triple3) -> rule2))]
("mouse" "eats" "mouse" "+")
((triple3) -> (rule2 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The squirrel does not see the cow.
False
2
inv-proof
[(((triple4) -> rule3))]
("squirrel" "sees" "cow" "-")
((triple4) -> (rule3 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The squirrel eats the mouse.
True
3
proof
[(((((triple4) -> rule3)) -> rule2))]
("squirrel" "eats" "mouse" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2
The squirrel does not eat the mouse.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2))]
("squirrel" "eats" "mouse" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2
The cow does not see the cow.
Unknown
inv-rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "cow" "-")
The cat sees the cow.
Unknown
rconc
[@1: The cat sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "cow" "+")
The cow does not eat the mouse.
Unknown
inv-rconc
[@2: The cow eats the mouse.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("cow" "eats" "mouse" "-")
The mouse needs the cow.
Unknown
random
[@0: The mouse needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cow" "+")
The squirrel does not need the cow.
Unknown
inv-random
[@0: The squirrel needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "cow" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
@0: The cat eats the cow.[(triple1)] The cow is cold.[(triple2)] The mouse sees the cow.[(triple3)] The squirrel is big.[(triple4)] @1: The mouse eats the mouse.[(((triple3) -> rule2))] The squirrel sees the cow.[(((triple4) -> rule3))] @2: The squirrel eats the mouse.[(((((triple4) -> rule3)) -> rule2))]
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple3
The squirrel is big.
("squirrel" "is" "big" "+")
triple4
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((triple3) -> (rule2 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
((triple4) -> (rule3 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2