The dog eats the lion. The dog is big. The dog is nice. The dog is red. The dog is rough. The dog is young. The dog needs the lion. The dog visits the lion. The lion eats the dog. The lion is big. The lion is nice. The lion is red. The lion is rough. The lion is young. The lion needs the dog. The lion visits the dog. If something visits the dog then it needs the lion. If something is rough and red then it needs the dog. If something needs the lion and it eats the dog then it visits the lion.
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
If something visits the dog then it needs the lion.
((("something" "visits" "dog" "+")) -> ("something" "needs" "lion" "+"))
If something is rough and red then it needs the dog.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "needs" "dog" "+"))
If something needs the lion and it eats the dog then it visits the lion.
((("something" "needs" "lion" "+") ("something" "eats" "dog" "+")) -> ("something" "visits" "lion" "+"))
The dog needs the lion.
True
1
proof
[(triple7)]
("dog" "needs" "lion" "+")
triple7
The lion does not visit the dog.
False
1
inv-proof
[(triple16)]
("lion" "visits" "dog" "-")
triple16
The dog needs the dog.
True
3
proof
[(((triple5 triple4) -> rule2))]
("dog" "needs" "dog" "+")
((triple5 triple4) -> (rule2 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog does not need the dog.
False
3
inv-proof
[(((triple5 triple4) -> rule2))]
("dog" "needs" "dog" "-")
((triple5 triple4) -> (rule2 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The lion visits the lion.
True
4
proof
[(((((triple16) -> rule1) triple9) -> rule3))]
("lion" "visits" "lion" "+")
((((triple16) -> (rule1 % int2)) triple9) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion does not visit the lion.
False
4
inv-proof
[(((((triple16) -> rule1) triple9) -> rule3))]
("lion" "visits" "lion" "-")
((((triple16) -> (rule1 % int2)) triple9) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
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 eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The dog eats the lion.[(triple1)] The dog is big.[(triple2)] The dog is nice.[(triple3)] The dog is red.[(triple4)] The dog is rough.[(triple5)] The dog is young.[(triple6)] The dog needs the lion.[(triple7)] The dog visits the lion.[(triple8)] The lion eats the dog.[(triple9)] The lion is big.[(triple10)] The lion is nice.[(triple11)] The lion is red.[(triple12)] The lion is rough.[(triple13)] The lion is young.[(triple14)] The lion needs the dog.[(triple15 OR ((triple13 triple12) -> rule2))] The lion visits the dog.[(triple16)] @1: The dog needs the dog.[(((triple5 triple4) -> rule2))] The lion needs the lion.[(((triple16) -> rule1))] @2: The lion visits the lion.[(((((triple16) -> rule1) triple9) -> rule3))]
The dog eats the lion.
("dog" "eats" "lion" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The dog is nice.
("dog" "is" "nice" "+")
triple3
The dog is red.
("dog" "is" "red" "+")
triple4
The dog is rough.
("dog" "is" "rough" "+")
triple5
The dog is young.
("dog" "is" "young" "+")
triple6
The dog needs the lion.
("dog" "needs" "lion" "+")
triple7
The dog visits the lion.
("dog" "visits" "lion" "+")
triple8
The lion eats the dog.
("lion" "eats" "dog" "+")
triple9
The lion is big.
("lion" "is" "big" "+")
triple10
The lion is nice.
("lion" "is" "nice" "+")
triple11
The lion is red.
("lion" "is" "red" "+")
triple12
The lion is rough.
("lion" "is" "rough" "+")
triple13
The lion is young.
("lion" "is" "young" "+")
triple14
The lion needs the dog.
("lion" "needs" "dog" "+")
triple15
((triple13 triple12) -> (rule2 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
triple16
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple5 triple4) -> (rule2 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple16) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
((((triple16) -> (rule1 % int2)) triple9) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2