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