The cow is big. The cow is cold. The cow is green. The cow is nice. The cow needs the squirrel. The cow sees the squirrel. The cow visits the squirrel. The squirrel is big. The squirrel is nice. The squirrel needs the cow. The squirrel sees the cow. The squirrel visits the cow. If someone is nice then they see the cow. If someone is cold and not big then they need the squirrel. If someone sees the cow and they see the squirrel then the squirrel is green.
The cow is big.
("cow" "is" "big" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
If someone is nice then they see the cow.
((("someone" "is" "nice" "+")) -> ("someone" "sees" "cow" "+"))
If someone is cold and not big then they need the squirrel.
((("someone" "is" "cold" "+") ("someone" "is" "big" "~")) -> ("someone" "needs" "squirrel" "+"))
If someone sees the cow and they see the squirrel then the squirrel is green.
((("someone" "sees" "cow" "+") ("someone" "sees" "squirrel" "+")) -> ("squirrel" "is" "green" "+"))
The squirrel sees the cow.
True
1
proof
[(triple11 OR ((triple9) -> rule1))]
("squirrel" "sees" "cow" "+")
triple11
((triple9) -> (rule1 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The cow does not see the squirrel.
False
1
inv-proof
[(triple6)]
("cow" "sees" "squirrel" "-")
triple6
The cow sees the cow.
True
2
proof
[(((triple4) -> rule1))]
("cow" "sees" "cow" "+")
((triple4) -> (rule1 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow does not see the cow.
False
2
inv-proof
[(((triple4) -> rule1))]
("cow" "sees" "cow" "-")
((triple4) -> (rule1 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The squirrel is green.
True
4
proof
[(((((triple4) -> rule1) triple6) -> rule3))]
("squirrel" "is" "green" "+")
((((triple4) -> (rule1 % int2)) triple6) -> (rule3 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The squirrel is not green.
False
4
inv-proof
[(((((triple4) -> rule1) triple6) -> rule3))]
("squirrel" "is" "green" "-")
((((triple4) -> (rule1 % int2)) triple6) -> (rule3 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The squirrel is young.
Unknown
random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
@0: The cow is big.[(triple1)] The cow is cold.[(triple2)] The cow is green.[(triple3)] The cow is nice.[(triple4)] The cow needs the squirrel.[(triple5)] The cow sees the squirrel.[(triple6)] The cow visits the squirrel.[(triple7)] The squirrel is big.[(triple8)] The squirrel is nice.[(triple9)] The squirrel needs the cow.[(triple10)] The squirrel sees the cow.[(triple11 OR ((triple9) -> rule1))] The squirrel visits the cow.[(triple12)] @1: The cow sees the cow.[(((triple4) -> rule1))] @2: The squirrel is green.[(((((triple4) -> rule1) triple6) -> rule3))]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The cow is green.
("cow" "is" "green" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
triple4
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple5
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple6
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple7
The squirrel is big.
("squirrel" "is" "big" "+")
triple8
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple9
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple10
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple11
((triple9) -> (rule1 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple12
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple4) -> (rule1 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
((((triple4) -> (rule1 % int2)) triple6) -> (rule3 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2