The cow chases the squirrel. The cow is blue. The cow is green. The cow is kind. The cow sees the squirrel. The cow visits the squirrel. The squirrel is nice. If something visits the squirrel then the squirrel chases the cow. If something chases the squirrel then it chases the cow. If something is cold then it visits the cow. If something sees the squirrel then it visits the squirrel. If something is cold and it sees the squirrel then it visits the squirrel. If something visits the squirrel then it sees the cow.
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
If something visits the squirrel then the squirrel chases the cow.
((("something" "visits" "squirrel" "+")) -> ("squirrel" "chases" "cow" "+"))
If something chases the squirrel then it chases the cow.
((("something" "chases" "squirrel" "+")) -> ("something" "chases" "cow" "+"))
If something is cold then it visits the cow.
((("something" "is" "cold" "+")) -> ("something" "visits" "cow" "+"))
If something sees the squirrel then it visits the squirrel.
((("something" "sees" "squirrel" "+")) -> ("something" "visits" "squirrel" "+"))
If something is cold and it sees the squirrel then it visits the squirrel.
((("something" "is" "cold" "+") ("something" "sees" "squirrel" "+")) -> ("something" "visits" "squirrel" "+"))
If something visits the squirrel then it sees the cow.
((("something" "visits" "squirrel" "+")) -> ("something" "sees" "cow" "+"))
The cow sees the squirrel.
True
1
proof
[(triple5)]
("cow" "sees" "squirrel" "+")
triple5
The cow does not see the squirrel.
False
1
inv-proof
[(triple5)]
("cow" "sees" "squirrel" "-")
triple5
The cow does not visit the cow.
Unknown
inv-rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "visits" "cow" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
@0: The cow chases the squirrel.[(triple1)] The cow is blue.[(triple2)] The cow is green.[(triple3)] The cow is kind.[(triple4)] The cow sees the squirrel.[(triple5)] The cow visits the squirrel.[(triple6 OR ((triple5) -> rule4))] The squirrel is nice.[(triple7)] @1: The cow chases the cow.[(((triple1) -> rule2))] The cow sees the cow.[(((triple6) -> rule6) OR ((((triple5) -> rule4)) -> rule6))] The squirrel chases the cow.[(((triple6) -> rule1) OR ((((triple5) -> rule4)) -> rule1))]
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow is green.
("cow" "is" "green" "+")
triple3
The cow is kind.
("cow" "is" "kind" "+")
triple4
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple5
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple6
((triple5) -> (rule4 % int1))
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple7
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple1) -> (rule2 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple6) -> (rule6 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule6 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
((triple6) -> (rule1 % int1))
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
int2