The dog is big. The dog is blue. The dog is cold. The dog is green. The dog is young. The dog needs the lion. The dog sees the lion. The dog visits the lion. The lion is not big. The lion is blue. The lion is cold. The lion is green. The lion does not need the dog. The lion sees the dog. The lion visits the dog. If someone is green then they do not need the dog. If someone visits the lion then they are green. If someone is cold and they do not visit the dog then they are not big.
The dog is big.
("dog" "is" "big" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion is not big.
("lion" "is" "big" "-")
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is green.
("lion" "is" "green" "+")
The lion does not need the dog.
("lion" "needs" "dog" "-")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
If someone is green then they do not need the dog.
((("someone" "is" "green" "+")) -> ("someone" "needs" "dog" "-"))
If someone visits the lion then they are green.
((("someone" "visits" "lion" "+")) -> ("someone" "is" "green" "+"))
If someone is cold and they do not visit the dog then they are not big.
((("someone" "is" "cold" "+") ("someone" "visits" "dog" "~")) -> ("someone" "is" "big" "-"))
The lion does not need the dog.
True
1
proof
[(triple13 OR ((triple12) -> rule1))]
("lion" "needs" "dog" "-")
triple13
((triple12) -> (rule1 % int1))
The lion does not need the dog.
("lion" "needs" "dog" "-")
int1
The dog is not young.
False
1
inv-proof
[(triple5)]
("dog" "is" "young" "-")
triple5
The dog does not need the dog.
True
2
proof
[(((triple4) -> rule1) OR ((((triple8) -> rule2)) -> rule1))]
("dog" "needs" "dog" "-")
((triple4) -> (rule1 % int1))
The dog does not need the dog.
("dog" "needs" "dog" "-")
int1
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
The dog does not need the dog.
("dog" "needs" "dog" "-")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog needs the dog.
False
2
inv-proof
[(((triple4) -> rule1) OR ((((triple8) -> rule2)) -> rule1))]
("dog" "needs" "dog" "+")
((triple4) -> (rule1 % int1))
The dog does not need the dog.
("dog" "needs" "dog" "-")
int1
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
The dog does not need the dog.
("dog" "needs" "dog" "-")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The dog is big.[(triple1)] The dog is blue.[(triple2)] The dog is cold.[(triple3)] The dog is green.[(triple4 OR ((triple8) -> rule2))] The dog is young.[(triple5)] The dog needs the lion.[(triple6)] The dog sees the lion.[(triple7)] The dog visits the lion.[(triple8)] The lion does not need the dog.[(triple13 OR ((triple12) -> rule1))] The lion is blue.[(triple10)] The lion is cold.[(triple11)] The lion is green.[(triple12)] The lion is not big.[(triple9)] The lion sees the dog.[(triple14)] The lion visits the dog.[(triple15)] @1: The dog does not need the dog.[(((triple4) -> rule1) OR ((((triple8) -> rule2)) -> rule1))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is blue.
("dog" "is" "blue" "+")
triple2
The dog is cold.
("dog" "is" "cold" "+")
triple3
The dog is green.
("dog" "is" "green" "+")
triple4
((triple8) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is young.
("dog" "is" "young" "+")
triple5
The dog needs the lion.
("dog" "needs" "lion" "+")
triple6
The dog sees the lion.
("dog" "sees" "lion" "+")
triple7
The dog visits the lion.
("dog" "visits" "lion" "+")
triple8
The lion does not need the dog.
("lion" "needs" "dog" "-")
triple13
((triple12) -> (rule1 % int1))
The lion does not need the dog.
("lion" "needs" "dog" "-")
int1
The lion is blue.
("lion" "is" "blue" "+")
triple10
The lion is cold.
("lion" "is" "cold" "+")
triple11
The lion is green.
("lion" "is" "green" "+")
triple12
The lion is not big.
("lion" "is" "big" "-")
triple9
The lion sees the dog.
("lion" "sees" "dog" "+")
triple14
The lion visits the dog.
("lion" "visits" "dog" "+")
triple15
The dog does not need the dog.
("dog" "needs" "dog" "-")
((triple4) -> (rule1 % int1))
The dog does not need the dog.
("dog" "needs" "dog" "-")
int1
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
The dog does not need the dog.
("dog" "needs" "dog" "-")
int1
The dog is green.
("dog" "is" "green" "+")
int2