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