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