The dog is big. The dog is nice. The dog is round. The dog is young. The dog likes the lion. The dog sees the lion. The dog visits the lion. The lion is big. The lion is cold. The lion is nice. The lion is round. The lion is young. The lion likes the dog. The lion sees the dog. The lion visits the dog. If something sees the dog then the dog sees the lion. All nice, big things are round. If the dog is round then the dog is nice. If the dog sees the lion then the dog likes the lion. If the lion likes the dog and the dog is big then the lion is round. If something sees the dog and the dog sees the lion then it sees the lion.
The dog is big.
("dog" "is" "big" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is round.
("dog" "is" "round" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is round.
("lion" "is" "round" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
If something sees the dog then the dog sees the lion.
((("something" "sees" "dog" "+")) -> ("dog" "sees" "lion" "+"))
All nice, big things are round.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If the dog is round then the dog is nice.
((("dog" "is" "round" "+")) -> ("dog" "is" "nice" "+"))
If the dog sees the lion then the dog likes the lion.
((("dog" "sees" "lion" "+")) -> ("dog" "likes" "lion" "+"))
If the lion likes the dog and the dog is big then the lion is round.
((("lion" "likes" "dog" "+") ("dog" "is" "big" "+")) -> ("lion" "is" "round" "+"))
If something sees the dog and the dog sees the lion then it sees the lion.
((("something" "sees" "dog" "+") ("dog" "sees" "lion" "+")) -> ("something" "sees" "lion" "+"))
The lion is cold.
True
1
proof
[(triple9)]
("lion" "is" "cold" "+")
triple9
The lion is not nice.
False
1
inv-proof
[(triple10)]
("lion" "is" "nice" "-")
triple10
The lion sees the lion.
True
3
proof
[(((triple14 triple6) -> rule6) OR ((triple14 ((triple14) -> rule1)) -> rule6))]
("lion" "sees" "lion" "+")
((triple14 triple6) -> (rule6 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
((triple14 ((triple14) -> (rule1 % int2))) -> (rule6 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
int2
The lion does not see the lion.
False
3
inv-proof
[(((triple14 triple6) -> rule6) OR ((triple14 ((triple14) -> rule1)) -> rule6))]
("lion" "sees" "lion" "-")
((triple14 triple6) -> (rule6 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
((triple14 ((triple14) -> (rule1 % int2))) -> (rule6 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
int2
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 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 cold.
Unknown
inv-random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The dog is big.[(triple1)] The dog is nice.[(triple2 OR ((triple3) -> rule3))] The dog is round.[(triple3 OR ((triple2 triple1) -> rule2))] The dog is young.[(triple4)] The dog likes the lion.[(triple5 OR ((triple6) -> rule4) OR ((((triple14) -> rule1)) -> rule4))] The dog sees the lion.[(triple6 OR ((triple14) -> rule1))] The dog visits the lion.[(triple7)] The lion is big.[(triple8)] The lion is cold.[(triple9)] The lion is nice.[(triple10)] The lion is round.[(triple11 OR ((triple10 triple8) -> rule2) OR ((triple13 triple1) -> rule5))] The lion is young.[(triple12)] The lion likes the dog.[(triple13)] The lion sees the dog.[(triple14)] The lion visits the dog.[(triple15)] @1: The lion sees the lion.[(((triple14 triple6) -> rule6) OR ((triple14 ((triple14) -> rule1)) -> rule6))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is nice.
("dog" "is" "nice" "+")
triple2
((triple3) -> (rule3 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is round.
("dog" "is" "round" "+")
triple3
((triple2 triple1) -> (rule2 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is young.
("dog" "is" "young" "+")
triple4
The dog likes the lion.
("dog" "likes" "lion" "+")
triple5
((triple6) -> (rule4 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
((((triple14) -> (rule1 % int2))) -> (rule4 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
int2
The dog sees the lion.
("dog" "sees" "lion" "+")
triple6
((triple14) -> (rule1 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
triple7
The lion is big.
("lion" "is" "big" "+")
triple8
The lion is cold.
("lion" "is" "cold" "+")
triple9
The lion is nice.
("lion" "is" "nice" "+")
triple10
The lion is round.
("lion" "is" "round" "+")
triple11
((triple10 triple8) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
((triple13 triple1) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is young.
("lion" "is" "young" "+")
triple12
The lion likes the dog.
("lion" "likes" "dog" "+")
triple13
The lion sees the dog.
("lion" "sees" "dog" "+")
triple14
The lion visits the dog.
("lion" "visits" "dog" "+")
triple15
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple14 triple6) -> (rule6 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
((triple14 ((triple14) -> (rule1 % int2))) -> (rule6 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
int2