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