The cat needs the lion. The cat needs the mouse. The dog chases the mouse. The dog is big. The dog is blue. The dog is green. The dog likes the cat. The lion is big. The lion likes the mouse. The lion needs the cat. The lion needs the mouse. The mouse is big. If something needs the lion then the lion likes the dog. If something likes the dog then the dog needs the lion.
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is green.
("dog" "is" "green" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The lion is big.
("lion" "is" "big" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse is big.
("mouse" "is" "big" "+")
If something needs the lion then the lion likes the dog.
((("something" "needs" "lion" "+")) -> ("lion" "likes" "dog" "+"))
If something likes the dog then the dog needs the lion.
((("something" "likes" "dog" "+")) -> ("dog" "needs" "lion" "+"))
The lion needs the cat.
True
1
proof
[(triple10)]
("lion" "needs" "cat" "+")
triple10
The lion does not need the cat.
False
1
inv-proof
[(triple10)]
("lion" "needs" "cat" "-")
triple10
The lion likes the dog.
True
2
proof
[(((triple1) -> rule1))]
("lion" "likes" "dog" "+")
((triple1) -> (rule1 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The lion does not like the dog.
False
2
inv-proof
[(((triple1) -> rule1))]
("lion" "likes" "dog" "-")
((triple1) -> (rule1 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The dog needs the lion.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("dog" "needs" "lion" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
int2
The dog does not need the lion.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("dog" "needs" "lion" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
int2
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The dog needs the mouse.
Unknown
random
[@0: The dog needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "mouse" "+")
The dog does not need the cat.
Unknown
inv-random
[@0: The dog needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cat" "-")
The mouse likes the cat.
Unknown
random
[@0: The mouse likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "cat" "+")
The lion does not need the dog.
Unknown
inv-random
[@0: The lion needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "dog" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The cat needs the lion.[(triple1)] The cat needs the mouse.[(triple2)] The dog chases the mouse.[(triple3)] The dog is big.[(triple4)] The dog is blue.[(triple5)] The dog is green.[(triple6)] The dog likes the cat.[(triple7)] The lion is big.[(triple8)] The lion likes the mouse.[(triple9)] The lion needs the cat.[(triple10)] The lion needs the mouse.[(triple11)] The mouse is big.[(triple12)] @1: The lion likes the dog.[(((triple1) -> rule1))] @2: The dog needs the lion.[(((((triple1) -> rule1)) -> rule2))]
The cat needs the lion.
("cat" "needs" "lion" "+")
triple1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple3
The dog is big.
("dog" "is" "big" "+")
triple4
The dog is blue.
("dog" "is" "blue" "+")
triple5
The dog is green.
("dog" "is" "green" "+")
triple6
The dog likes the cat.
("dog" "likes" "cat" "+")
triple7
The lion is big.
("lion" "is" "big" "+")
triple8
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple9
The lion needs the cat.
("lion" "needs" "cat" "+")
triple10
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple11
The mouse is big.
("mouse" "is" "big" "+")
triple12
The lion likes the dog.
("lion" "likes" "dog" "+")
((triple1) -> (rule1 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
int2