The dog eats the lion. The dog visits the lion. The lion eats the squirrel. The lion is red. The lion is young. The lion sees the squirrel. The lion visits the dog. The lion visits the squirrel. The squirrel is round. The squirrel is young. The squirrel sees the dog. The squirrel visits the dog. If something is red and it sees the dog then the dog is not kind. If the lion visits the squirrel and the lion does not eat the squirrel then the lion does not visit the dog. If something visits the dog and the dog eats the squirrel then the dog is red. If something visits the dog and the dog sees the lion then the dog is not red. If something eats the squirrel then the squirrel is red. If something sees the lion and it does not see the dog then it eats the dog.
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is young.
("lion" "is" "young" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If something is red and it sees the dog then the dog is not kind.
((("something" "is" "red" "+") ("something" "sees" "dog" "+")) -> ("dog" "is" "kind" "-"))
If the lion visits the squirrel and the lion does not eat the squirrel then the lion does not visit the dog.
((("lion" "visits" "squirrel" "+") ("lion" "eats" "squirrel" "~")) -> ("lion" "visits" "dog" "-"))
If something visits the dog and the dog eats the squirrel then the dog is red.
((("something" "visits" "dog" "+") ("dog" "eats" "squirrel" "+")) -> ("dog" "is" "red" "+"))
If something visits the dog and the dog sees the lion then the dog is not red.
((("something" "visits" "dog" "+") ("dog" "sees" "lion" "+")) -> ("dog" "is" "red" "-"))
If something eats the squirrel then the squirrel is red.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "is" "red" "+"))
If something sees the lion and it does not see the dog then it eats the dog.
((("something" "sees" "lion" "+") ("something" "sees" "dog" "~")) -> ("something" "eats" "dog" "+"))
The squirrel is round.
True
1
proof
[(triple9)]
("squirrel" "is" "round" "+")
triple9
The dog does not visit the lion.
False
1
inv-proof
[(triple2)]
("dog" "visits" "lion" "-")
triple2
The squirrel is red.
True
2
proof
[(((triple3) -> rule5))]
("squirrel" "is" "red" "+")
((triple3) -> (rule5 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is not red.
False
2
inv-proof
[(((triple3) -> rule5))]
("squirrel" "is" "red" "-")
((triple3) -> (rule5 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The dog is not kind.
True
4
proof
[(((((triple3) -> rule5) triple11) -> rule1))]
("dog" "is" "kind" "-")
((((triple3) -> (rule5 % int2)) triple11) -> (rule1 % int1))
The dog is not kind.
("dog" "is" "kind" "-")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The dog is kind.
False
4
inv-proof
[(((((triple3) -> rule5) triple11) -> rule1))]
("dog" "is" "kind" "+")
((((triple3) -> (rule5 % int2)) triple11) -> (rule1 % int1))
The dog is not kind.
("dog" "is" "kind" "-")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The dog does not eat the dog.
Unknown
inv-rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "eats" "dog" "-")
The dog is red.
Unknown
rconc
[@1: The dog is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "red" "+")
The lion does not eat the dog.
Unknown
inv-rconc
[@1: The lion eats the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "eats" "dog" "-")
The squirrel eats the lion.
Unknown
random
[@0: The squirrel eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "lion" "+")
The dog does not visit the squirrel.
Unknown
inv-random
[@0: The dog visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "squirrel" "-")
The dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
@0: The dog eats the lion.[(triple1)] The dog visits the lion.[(triple2)] The lion eats the squirrel.[(triple3)] The lion is red.[(triple4)] The lion is young.[(triple5)] The lion sees the squirrel.[(triple6)] The lion visits the dog.[(triple7)] The lion visits the squirrel.[(triple8)] The squirrel is round.[(triple9)] The squirrel is young.[(triple10)] The squirrel sees the dog.[(triple11)] The squirrel visits the dog.[(triple12)] @1: The squirrel is red.[(((triple3) -> rule5))] @2: The dog is not kind.[(((((triple3) -> rule5) triple11) -> rule1))]
The dog eats the lion.
("dog" "eats" "lion" "+")
triple1
The dog visits the lion.
("dog" "visits" "lion" "+")
triple2
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple3
The lion is red.
("lion" "is" "red" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple6
The lion visits the dog.
("lion" "visits" "dog" "+")
triple7
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple8
The squirrel is round.
("squirrel" "is" "round" "+")
triple9
The squirrel is young.
("squirrel" "is" "young" "+")
triple10
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple11
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple12
The squirrel is red.
("squirrel" "is" "red" "+")
((triple3) -> (rule5 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The dog is not kind.
("dog" "is" "kind" "-")
((((triple3) -> (rule5 % int2)) triple11) -> (rule1 % int1))
The dog is not kind.
("dog" "is" "kind" "-")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2