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