The dog is cold. The dog is round. The dog needs the lion. The dog sees the lion. The dog sees the squirrel. The lion is not blue. The lion is round. The lion needs the dog. The lion sees the dog. The lion does not see the squirrel. The squirrel is not blue. The squirrel is not round. The squirrel likes the dog. The squirrel does not need the dog. The squirrel sees the dog. The squirrel sees the lion. All round things are cold. If something likes the lion then it does not need the squirrel. If something needs the squirrel and it is not blue then it does not like the dog. If something likes the squirrel and it sees the lion then the squirrel does not need the lion. If something needs the lion then the lion needs the squirrel. If something is blue and it does not like the lion then it is not red.
The dog is cold.
("dog" "is" "cold" "+")
The dog is round.
("dog" "is" "round" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The lion is not blue.
("lion" "is" "blue" "-")
The lion is round.
("lion" "is" "round" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion does not see the squirrel.
("lion" "sees" "squirrel" "-")
The squirrel is not blue.
("squirrel" "is" "blue" "-")
The squirrel is not round.
("squirrel" "is" "round" "-")
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
The squirrel does not need the dog.
("squirrel" "needs" "dog" "-")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
All round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If something likes the lion then it does not need the squirrel.
((("something" "likes" "lion" "+")) -> ("something" "needs" "squirrel" "-"))
If something needs the squirrel and it is not blue then it does not like the dog.
((("something" "needs" "squirrel" "+") ("something" "is" "blue" "~")) -> ("something" "likes" "dog" "-"))
If something likes the squirrel and it sees the lion then the squirrel does not need the lion.
((("something" "likes" "squirrel" "+") ("something" "sees" "lion" "+")) -> ("squirrel" "needs" "lion" "-"))
If something needs the lion then the lion needs the squirrel.
((("something" "needs" "lion" "+")) -> ("lion" "needs" "squirrel" "+"))
If something is blue and it does not like the lion then it is not red.
((("something" "is" "blue" "+") ("something" "likes" "lion" "~")) -> ("something" "is" "red" "-"))
The lion does not see the squirrel.
True
1
proof
[(triple10)]
("lion" "sees" "squirrel" "-")
triple10
The lion sees the squirrel.
False
1
inv-proof
[(triple10)]
("lion" "sees" "squirrel" "+")
triple10
The lion is cold.
True
2
proof
[(((triple7) -> rule1))]
("lion" "is" "cold" "+")
((triple7) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is not cold.
False
2
inv-proof
[(((triple7) -> rule1))]
("lion" "is" "cold" "-")
((triple7) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion does not like the dog.
True
4
proof
[(((((triple3) -> rule5) triple6) -> rule3))]
("lion" "likes" "dog" "-")
((((triple3) -> (rule5 % int2)) triple6) -> (rule3 % int1))
The lion does not like the dog.
("lion" "likes" "dog" "-")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The lion likes the dog.
False
4
inv-proof
[(((((triple3) -> rule5) triple6) -> rule3))]
("lion" "likes" "dog" "+")
((((triple3) -> (rule5 % int2)) triple6) -> (rule3 % int1))
The lion does not like the dog.
("lion" "likes" "dog" "-")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The squirrel is not cold.
Unknown
inv-rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "cold" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The dog is not red.
Unknown
inv-random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "-")
The dog likes the squirrel.
Unknown
random
[@0: The dog likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "squirrel" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The squirrel is red.
Unknown
random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "+")
@0: The dog is cold.[(triple1 OR ((triple2) -> rule1))] The dog is round.[(triple2)] The dog needs the lion.[(triple3)] The dog sees the lion.[(triple4)] The dog sees the squirrel.[(triple5)] The lion does not see the squirrel.[(triple10)] The lion is not blue.[(triple6)] The lion is round.[(triple7)] The lion needs the dog.[(triple8)] The lion sees the dog.[(triple9)] The squirrel does not need the dog.[(triple14)] The squirrel is not blue.[(triple11)] The squirrel is not round.[(triple12)] The squirrel likes the dog.[(triple13)] The squirrel sees the dog.[(triple15)] The squirrel sees the lion.[(triple16)] @1: The lion is cold.[(((triple7) -> rule1))] The lion needs the squirrel.[(((triple3) -> rule5))] @2: The lion does not like the dog.[(((((triple3) -> rule5) triple6) -> rule3))]
The dog is cold.
("dog" "is" "cold" "+")
triple1
((triple2) -> (rule1 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is round.
("dog" "is" "round" "+")
triple2
The dog needs the lion.
("dog" "needs" "lion" "+")
triple3
The dog sees the lion.
("dog" "sees" "lion" "+")
triple4
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple5
The lion does not see the squirrel.
("lion" "sees" "squirrel" "-")
triple10
The lion is not blue.
("lion" "is" "blue" "-")
triple6
The lion is round.
("lion" "is" "round" "+")
triple7
The lion needs the dog.
("lion" "needs" "dog" "+")
triple8
The lion sees the dog.
("lion" "sees" "dog" "+")
triple9
The squirrel does not need the dog.
("squirrel" "needs" "dog" "-")
triple14
The squirrel is not blue.
("squirrel" "is" "blue" "-")
triple11
The squirrel is not round.
("squirrel" "is" "round" "-")
triple12
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
triple13
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple15
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple16
The lion is cold.
("lion" "is" "cold" "+")
((triple7) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
((triple3) -> (rule5 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The lion does not like the dog.
("lion" "likes" "dog" "-")
((((triple3) -> (rule5 % int2)) triple6) -> (rule3 % int1))
The lion does not like the dog.
("lion" "likes" "dog" "-")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2