The dog is big. The dog is young. The dog sees the lion. The lion is green. The lion likes the dog. The lion needs the dog. The lion sees the dog. If something is green then it likes the dog. If something is big then it sees the dog. Green, cold things are big. If something needs the dog and it is not green then the dog sees the lion. If the dog is nice and the lion does not see the dog then the dog does not need the lion. If something needs the lion and it is not young then the lion does not need the dog.
The dog is big.
("dog" "is" "big" "+")
The dog is young.
("dog" "is" "young" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion is green.
("lion" "is" "green" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
If something is green then it likes the dog.
((("something" "is" "green" "+")) -> ("something" "likes" "dog" "+"))
If something is big then it sees the dog.
((("something" "is" "big" "+")) -> ("something" "sees" "dog" "+"))
Green, cold things are big.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If something needs the dog and it is not green then the dog sees the lion.
((("something" "needs" "dog" "+") ("something" "is" "green" "~")) -> ("dog" "sees" "lion" "+"))
If the dog is nice and the lion does not see the dog then the dog does not need the lion.
((("dog" "is" "nice" "+") ("lion" "sees" "dog" "~")) -> ("dog" "needs" "lion" "-"))
If something needs the lion and it is not young then the lion does not need the dog.
((("something" "needs" "lion" "+") ("something" "is" "young" "~")) -> ("lion" "needs" "dog" "-"))
The dog is big.
True
1
proof
[(triple1)]
("dog" "is" "big" "+")
triple1
The dog does not see the lion.
False
1
inv-proof
[(triple3)]
("dog" "sees" "lion" "-")
triple3
The dog sees the dog.
True
2
proof
[(((triple1) -> rule2))]
("dog" "sees" "dog" "+")
((triple1) -> (rule2 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog does not see the dog.
False
2
inv-proof
[(((triple1) -> rule2))]
("dog" "sees" "dog" "-")
((triple1) -> (rule2 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog does not like the dog.
Unknown
inv-rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "likes" "dog" "-")
The lion is big.
Unknown
rconc
[@1: The lion is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "big" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
@0: The dog is big.[(triple1)] The dog is young.[(triple2)] The dog sees the lion.[(triple3)] The lion is green.[(triple4)] The lion likes the dog.[(triple5 OR ((triple4) -> rule1))] The lion needs the dog.[(triple6)] The lion sees the dog.[(triple7)] @1: The dog sees the dog.[(((triple1) -> rule2))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is young.
("dog" "is" "young" "+")
triple2
The dog sees the lion.
("dog" "sees" "lion" "+")
triple3
The lion is green.
("lion" "is" "green" "+")
triple4
The lion likes the dog.
("lion" "likes" "dog" "+")
triple5
((triple4) -> (rule1 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
triple6
The lion sees the dog.
("lion" "sees" "dog" "+")
triple7
The dog sees the dog.
("dog" "sees" "dog" "+")
((triple1) -> (rule2 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1