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