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