The dog does not eat the lion. The dog is big. The dog is blue. The lion eats the dog. The lion eats the squirrel. The lion is big. The squirrel is blue. If something visits the dog and it is not big then it eats the lion. If something sees the dog and it is cold then it is blue. If something is cold and it visits the squirrel then the squirrel is not cold. If something visits the dog then the dog sees the squirrel. If something eats the lion and the lion eats the squirrel then the squirrel does not see the dog. If something eats the squirrel then the squirrel visits the dog.
The dog does not eat the lion.
("dog" "eats" "lion" "-")
The dog is big.
("dog" "is" "big" "+")
The dog is blue.
("dog" "is" "blue" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion is big.
("lion" "is" "big" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
If something visits the dog and it is not big then it eats the lion.
((("something" "visits" "dog" "+") ("something" "is" "big" "~")) -> ("something" "eats" "lion" "+"))
If something sees the dog and it is cold then it is blue.
((("something" "sees" "dog" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something is cold and it visits the squirrel then the squirrel is not cold.
((("something" "is" "cold" "+") ("something" "visits" "squirrel" "+")) -> ("squirrel" "is" "cold" "-"))
If something visits the dog then the dog sees the squirrel.
((("something" "visits" "dog" "+")) -> ("dog" "sees" "squirrel" "+"))
If something eats the lion and the lion eats the squirrel then the squirrel does not see the dog.
((("something" "eats" "lion" "+") ("lion" "eats" "squirrel" "+")) -> ("squirrel" "sees" "dog" "-"))
If something eats the squirrel then the squirrel visits the dog.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "visits" "dog" "+"))
The dog is blue.
True
1
proof
[(triple3)]
("dog" "is" "blue" "+")
triple3
The dog is not big.
False
1
inv-proof
[(triple2)]
("dog" "is" "big" "-")
triple2
The squirrel visits the dog.
True
2
proof
[(((triple5) -> rule6))]
("squirrel" "visits" "dog" "+")
((triple5) -> (rule6 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The squirrel does not visit the dog.
False
2
inv-proof
[(((triple5) -> rule6))]
("squirrel" "visits" "dog" "-")
((triple5) -> (rule6 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The dog sees the squirrel.
True
3
proof
[(((((triple5) -> rule6)) -> rule4))]
("dog" "sees" "squirrel" "+")
((((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
The dog does not see the squirrel.
False
3
inv-proof
[(((((triple5) -> rule6)) -> rule4))]
("dog" "sees" "squirrel" "-")
((((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
The squirrel does not eat the lion.
Unknown
inv-rconc
[@1: The squirrel eats the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "eats" "lion" "-")
The lion is blue.
Unknown
rconc
[@1: The lion is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "blue" "+")
The lion does not eat the lion.
Unknown
inv-rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "eats" "lion" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
The squirrel is not young.
Unknown
inv-random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The dog does not eat the lion.[(triple1)] The dog is big.[(triple2)] The dog is blue.[(triple3)] The lion eats the dog.[(triple4)] The lion eats the squirrel.[(triple5)] The lion is big.[(triple6)] The squirrel is blue.[(triple7)] @1: The squirrel visits the dog.[(((triple5) -> rule6))] @2: The dog sees the squirrel.[(((((triple5) -> rule6)) -> rule4))]
The dog does not eat the lion.
("dog" "eats" "lion" "-")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The dog is blue.
("dog" "is" "blue" "+")
triple3
The lion eats the dog.
("lion" "eats" "dog" "+")
triple4
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple5
The lion is big.
("lion" "is" "big" "+")
triple6
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple7
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
((triple5) -> (rule6 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
((((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2