The dog chases the lion. The dog is blue. The dog is cold. The dog is green. The dog is red. The dog is young. The dog needs the lion. The dog sees the lion. The lion chases the dog. The lion is blue. The lion is cold. The lion is green. The lion is red. The lion needs the dog. The lion sees the dog. If the dog sees the lion and the dog chases the lion then the dog is young. If something chases the lion then the lion is cold. If something is green then it sees the lion. If something chases the lion and it sees the dog then the lion is green. If something chases the dog then the dog is blue. If something sees the lion then it chases the lion. If something sees the lion and it is young then it is green. If something chases the lion then it is green.
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is red.
("lion" "is" "red" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
If the dog sees the lion and the dog chases the lion then the dog is young.
((("dog" "sees" "lion" "+") ("dog" "chases" "lion" "+")) -> ("dog" "is" "young" "+"))
If something chases the lion then the lion is cold.
((("something" "chases" "lion" "+")) -> ("lion" "is" "cold" "+"))
If something is green then it sees the lion.
((("something" "is" "green" "+")) -> ("something" "sees" "lion" "+"))
If something chases the lion and it sees the dog then the lion is green.
((("something" "chases" "lion" "+") ("something" "sees" "dog" "+")) -> ("lion" "is" "green" "+"))
If something chases the dog then the dog is blue.
((("something" "chases" "dog" "+")) -> ("dog" "is" "blue" "+"))
If something sees the lion then it chases the lion.
((("something" "sees" "lion" "+")) -> ("something" "chases" "lion" "+"))
If something sees the lion and it is young then it is green.
((("something" "sees" "lion" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If something chases the lion then it is green.
((("something" "chases" "lion" "+")) -> ("something" "is" "green" "+"))
The lion is cold.
True
1
proof
[(triple11 OR ((triple1) -> rule2) OR ((((triple8) -> rule6)) -> rule2) OR ((((((triple12) -> rule3)) -> rule6)) -> rule2) OR ((((((triple4) -> rule3)) -> rule6)) -> rule2))]
("lion" "is" "cold" "+")
triple11
((triple1) -> (rule2 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
((((triple8) -> (rule6 % int2))) -> (rule2 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
int2
((((((triple12) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion sees the lion.
("lion" "sees" "lion" "+")
int3
((((((triple4) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
int2
The dog sees the lion.
("dog" "sees" "lion" "+")
int3
The dog does not need the lion.
False
1
inv-proof
[(triple7)]
("dog" "needs" "lion" "-")
triple7
The lion sees the lion.
True
2
proof
[(((triple12) -> rule3))]
("lion" "sees" "lion" "+")
((triple12) -> (rule3 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion does not see the lion.
False
2
inv-proof
[(((triple12) -> rule3))]
("lion" "sees" "lion" "-")
((triple12) -> (rule3 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion chases the lion.
True
3
proof
[(((((triple12) -> rule3)) -> rule6))]
("lion" "chases" "lion" "+")
((((triple12) -> (rule3 % int2))) -> (rule6 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The lion does not chase the lion.
False
3
inv-proof
[(((((triple12) -> rule3)) -> rule6))]
("lion" "chases" "lion" "-")
((((triple12) -> (rule3 % int2))) -> (rule6 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The dog chases the lion.[(triple1 OR ((triple8) -> rule6) OR ((((triple4) -> rule3)) -> rule6))] The dog is blue.[(triple2 OR ((triple9) -> rule5))] The dog is cold.[(triple3)] The dog is green.[(triple4 OR ((triple1) -> rule8) OR ((triple8 triple6) -> rule7) OR ((((triple8) -> rule6)) -> rule8) OR ((triple8 ((triple8 triple1) -> rule1)) -> rule7) OR ((triple8 ((triple8 ((triple8) -> rule6)) -> rule1)) -> rule7))] The dog is red.[(triple5)] The dog is young.[(triple6 OR ((triple8 triple1) -> rule1) OR ((triple8 ((triple8) -> rule6)) -> rule1) OR ((((triple4) -> rule3) triple1) -> rule1) OR ((((triple4) -> rule3) ((triple8) -> rule6)) -> rule1) OR ((triple8 ((((triple4) -> rule3)) -> rule6)) -> rule1) OR ((((((triple1) -> rule8)) -> rule3) triple1) -> rule1) OR ((((triple4) -> rule3) ((((triple4) -> rule3)) -> rule6)) -> rule1) OR ((((((triple1) -> rule8)) -> rule3) ((triple8) -> rule6)) -> rule1) OR ((((((triple1) -> rule8)) -> rule3) ((((triple4) -> rule3)) -> rule6)) -> rule1))] The dog needs the lion.[(triple7)] The dog sees the lion.[(triple8 OR ((triple4) -> rule3) OR ((((triple1) -> rule8)) -> rule3))] The lion chases the dog.[(triple9)] The lion is blue.[(triple10)] The lion is cold.[(triple11 OR ((triple1) -> rule2) OR ((((triple8) -> rule6)) -> rule2) OR ((((((triple12) -> rule3)) -> rule6)) -> rule2) OR ((((((triple4) -> rule3)) -> rule6)) -> rule2))] The lion is green.[(triple12)] The lion is red.[(triple13)] The lion needs the dog.[(triple14)] The lion sees the dog.[(triple15)] @1: The lion sees the lion.[(((triple12) -> rule3))] @2: The lion chases the lion.[(((((triple12) -> rule3)) -> rule6))]
The dog chases the lion.
("dog" "chases" "lion" "+")
triple1
((triple8) -> (rule6 % int1))
The dog chases the lion.
("dog" "chases" "lion" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
The dog chases the lion.
("dog" "chases" "lion" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
triple2
((triple9) -> (rule5 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
triple3
The dog is green.
("dog" "is" "green" "+")
triple4
((triple1) -> (rule8 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
((triple8 triple6) -> (rule7 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
((((triple8) -> (rule6 % int2))) -> (rule8 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
int2
((triple8 ((triple8 triple1) -> (rule1 % int2))) -> (rule7 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
((triple8 ((triple8 ((triple8) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog chases the lion.
("dog" "chases" "lion" "+")
int3
The dog is red.
("dog" "is" "red" "+")
triple5
The dog is young.
("dog" "is" "young" "+")
triple6
((triple8 triple1) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
((triple8 ((triple8) -> (rule6 % int2))) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
int2
((((triple4) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
int2
((((triple4) -> (rule3 % int3)) ((triple8) -> (rule6 % int2))) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
int2
The dog sees the lion.
("dog" "sees" "lion" "+")
int3
((triple8 ((((triple4) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
int2
The dog sees the lion.
("dog" "sees" "lion" "+")
int3
((((((triple1) -> (rule8 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
int2
The dog is green.
("dog" "is" "green" "+")
int3
((((triple4) -> (rule3 % int3)) ((((triple4) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
int2
The dog sees the lion.
("dog" "sees" "lion" "+")
int3
((((((triple1) -> (rule8 % int4))) -> (rule3 % int3)) ((triple8) -> (rule6 % int2))) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
int2
The dog sees the lion.
("dog" "sees" "lion" "+")
int3
The dog is green.
("dog" "is" "green" "+")
int4
((((((triple1) -> (rule8 % int4))) -> (rule3 % int3)) ((((triple4) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
int2
The dog sees the lion.
("dog" "sees" "lion" "+")
int3
The dog is green.
("dog" "is" "green" "+")
int4
The dog needs the lion.
("dog" "needs" "lion" "+")
triple7
The dog sees the lion.
("dog" "sees" "lion" "+")
triple8
((triple4) -> (rule3 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
triple9
The lion is blue.
("lion" "is" "blue" "+")
triple10
The lion is cold.
("lion" "is" "cold" "+")
triple11
((triple1) -> (rule2 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
((((triple8) -> (rule6 % int2))) -> (rule2 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
int2
((((((triple12) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion sees the lion.
("lion" "sees" "lion" "+")
int3
((((((triple4) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
int2
The dog sees the lion.
("dog" "sees" "lion" "+")
int3
The lion is green.
("lion" "is" "green" "+")
triple12
The lion is red.
("lion" "is" "red" "+")
triple13
The lion needs the dog.
("lion" "needs" "dog" "+")
triple14
The lion sees the dog.
("lion" "sees" "dog" "+")
triple15
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple12) -> (rule3 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
((((triple12) -> (rule3 % int2))) -> (rule6 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2