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