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