The dog chases the lion. The dog is big. The dog is green. The dog is kind. The dog likes the lion. The dog needs the lion. The lion is cold. The lion is green. The lion likes the dog. The lion needs the dog. If someone is green then they need the lion. If someone likes the lion and they like the dog then the dog likes the lion. If someone likes the dog then they chase the lion. If someone likes the lion then the lion needs the dog. If someone needs the lion then they like the lion. If someone is cold then they need the lion.
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is green.
("lion" "is" "green" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
If someone is green then they need the lion.
((("someone" "is" "green" "+")) -> ("someone" "needs" "lion" "+"))
If someone likes the lion and they like the dog then the dog likes the lion.
((("someone" "likes" "lion" "+") ("someone" "likes" "dog" "+")) -> ("dog" "likes" "lion" "+"))
If someone likes the dog then they chase the lion.
((("someone" "likes" "dog" "+")) -> ("someone" "chases" "lion" "+"))
If someone likes the lion then the lion needs the dog.
((("someone" "likes" "lion" "+")) -> ("lion" "needs" "dog" "+"))
If someone needs the lion then they like the lion.
((("someone" "needs" "lion" "+")) -> ("someone" "likes" "lion" "+"))
If someone is cold then they need the lion.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "lion" "+"))
The dog is kind.
True
1
proof
[(triple4)]
("dog" "is" "kind" "+")
triple4
The lion is not green.
False
1
inv-proof
[(triple8)]
("lion" "is" "green" "-")
triple8
The lion chases the lion.
True
2
proof
[(((triple9) -> rule3))]
("lion" "chases" "lion" "+")
((triple9) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion does not need the lion.
False
2
inv-proof
[(((triple7) -> rule6) OR ((triple8) -> rule1))]
("lion" "needs" "lion" "-")
((triple7) -> (rule6 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
((triple8) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion likes the lion.
True
3
proof
[(((((triple7) -> rule6)) -> rule5) OR ((((triple8) -> rule1)) -> rule5))]
("lion" "likes" "lion" "+")
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
((((triple8) -> (rule1 % int2))) -> (rule5 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion does not like the lion.
False
3
inv-proof
[(((((triple7) -> rule6)) -> rule5) OR ((((triple8) -> rule1)) -> rule5))]
("lion" "likes" "lion" "-")
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
((((triple8) -> (rule1 % int2))) -> (rule5 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is not big.
Unknown
inv-random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "-")
The lion is kind.
Unknown
random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The dog is not cold.
Unknown
inv-random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "-")
The lion chases the dog.
Unknown
random
[@0: The lion chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "dog" "+")
@0: The dog chases the lion.[(triple1)] The dog is big.[(triple2)] The dog is green.[(triple3)] The dog is kind.[(triple4)] The dog likes the lion.[(triple5 OR ((triple6) -> rule5) OR ((((triple3) -> rule1)) -> rule5) OR ((((((triple7) -> rule6)) -> rule5) triple9) -> rule2) OR ((((((triple8) -> rule1)) -> rule5) triple9) -> rule2))] The dog needs the lion.[(triple6 OR ((triple3) -> rule1))] The lion is cold.[(triple7)] The lion is green.[(triple8)] The lion likes the dog.[(triple9)] The lion needs the dog.[(triple10 OR ((triple5) -> rule4) OR ((((triple6) -> rule5)) -> rule4) OR ((((((triple3) -> rule1)) -> rule5)) -> rule4) OR ((((((triple7) -> rule6)) -> rule5)) -> rule4) OR ((((((triple8) -> rule1)) -> rule5)) -> rule4) OR ((((((((triple7) -> rule6)) -> rule5) triple9) -> rule2)) -> rule4) OR ((((((((triple8) -> rule1)) -> rule5) triple9) -> rule2)) -> rule4))] @1: The lion chases the lion.[(((triple9) -> rule3))] The lion needs the lion.[(((triple7) -> rule6) OR ((triple8) -> rule1))] @2: The lion likes the lion.[(((((triple7) -> rule6)) -> rule5) OR ((((triple8) -> rule1)) -> rule5))]
The dog chases the lion.
("dog" "chases" "lion" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The dog is green.
("dog" "is" "green" "+")
triple3
The dog is kind.
("dog" "is" "kind" "+")
triple4
The dog likes the lion.
("dog" "likes" "lion" "+")
triple5
((triple6) -> (rule5 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
((((((triple7) -> (rule6 % int3))) -> (rule5 % int2)) triple9) -> (rule2 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
((((((triple8) -> (rule1 % int3))) -> (rule5 % int2)) triple9) -> (rule2 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
The dog needs the lion.
("dog" "needs" "lion" "+")
triple6
((triple3) -> (rule1 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
triple7
The lion is green.
("lion" "is" "green" "+")
triple8
The lion likes the dog.
("lion" "likes" "dog" "+")
triple9
The lion needs the dog.
("lion" "needs" "dog" "+")
triple10
((triple5) -> (rule4 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
The dog needs the lion.
("dog" "needs" "lion" "+")
int3
((((((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
((((((triple8) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
((((((((triple7) -> (rule6 % int4))) -> (rule5 % int3)) triple9) -> (rule2 % int2))) -> (rule4 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The lion needs the lion.
("lion" "needs" "lion" "+")
int4
((((((((triple8) -> (rule1 % int4))) -> (rule5 % int3)) triple9) -> (rule2 % int2))) -> (rule4 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The lion needs the lion.
("lion" "needs" "lion" "+")
int4
The lion chases the lion.
("lion" "chases" "lion" "+")
((triple9) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple7) -> (rule6 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
((triple8) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
((((triple8) -> (rule1 % int2))) -> (rule5 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2