The cow chases the lion. The cow is red. The cow is round. The cow is young. The cow sees the lion. The cow visits the lion. The lion chases the cow. The lion is blue. The lion is young. The lion visits the cow. If someone is young then they visit the lion. If the lion is young and the lion visits the cow then the lion is rough. If the cow is blue then the cow chases the lion. If someone is blue and they visit the cow then the cow visits the lion. If someone sees the cow and they chase the cow then the cow is red. If someone visits the lion and they see the lion then they chase the cow. If someone chases the lion and they see the lion then they see the cow. If someone is rough and round then they visit the lion.
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is round.
("cow" "is" "round" "+")
The cow is young.
("cow" "is" "young" "+")
The cow sees the lion.
("cow" "sees" "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 young.
("lion" "is" "young" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
If someone is young then they visit the lion.
((("someone" "is" "young" "+")) -> ("someone" "visits" "lion" "+"))
If the lion is young and the lion visits the cow then the lion is rough.
((("lion" "is" "young" "+") ("lion" "visits" "cow" "+")) -> ("lion" "is" "rough" "+"))
If the cow is blue then the cow chases the lion.
((("cow" "is" "blue" "+")) -> ("cow" "chases" "lion" "+"))
If someone is blue and they visit the cow then the cow visits the lion.
((("someone" "is" "blue" "+") ("someone" "visits" "cow" "+")) -> ("cow" "visits" "lion" "+"))
If someone sees the cow and they chase the cow then the cow is red.
((("someone" "sees" "cow" "+") ("someone" "chases" "cow" "+")) -> ("cow" "is" "red" "+"))
If someone visits the lion and they see the lion then they chase the cow.
((("someone" "visits" "lion" "+") ("someone" "sees" "lion" "+")) -> ("someone" "chases" "cow" "+"))
If someone chases the lion and they see the lion then they see the cow.
((("someone" "chases" "lion" "+") ("someone" "sees" "lion" "+")) -> ("someone" "sees" "cow" "+"))
If someone is rough and round then they visit the lion.
((("someone" "is" "rough" "+") ("someone" "is" "round" "+")) -> ("someone" "visits" "lion" "+"))
The lion is blue.
True
1
proof
[(triple8)]
("lion" "is" "blue" "+")
triple8
The cow is not round.
False
1
inv-proof
[(triple3)]
("cow" "is" "round" "-")
triple3
The cow chases the cow.
True
3
proof
[(((triple6 triple5) -> rule6) OR ((((triple4) -> rule1) triple5) -> rule6) OR ((((triple8 triple10) -> rule4) triple5) -> rule6))]
("cow" "chases" "cow" "+")
((triple6 triple5) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
((((triple4) -> (rule1 % int2)) triple5) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
int2
((((triple8 triple10) -> (rule4 % int2)) triple5) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
int2
The lion does not visit the lion.
False
2
inv-proof
[(((triple9) -> rule1))]
("lion" "visits" "lion" "-")
((triple9) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion does not see the cow.
Unknown
inv-rconc
[@1: The lion sees the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "sees" "cow" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
@0: The cow chases the lion.[(triple1)] The cow is red.[(triple2 OR ((((triple1 triple5) -> rule7) ((triple6 triple5) -> rule6)) -> rule5) OR ((((triple1 triple5) -> rule7) ((((triple4) -> rule1) triple5) -> rule6)) -> rule5) OR ((((triple1 triple5) -> rule7) ((((triple8 triple10) -> rule4) triple5) -> rule6)) -> rule5))] The cow is round.[(triple3)] The cow is young.[(triple4)] The cow sees the lion.[(triple5)] The cow visits the lion.[(triple6 OR ((triple4) -> rule1) OR ((triple8 triple10) -> rule4))] The lion chases the cow.[(triple7)] The lion is blue.[(triple8)] The lion is young.[(triple9)] The lion visits the cow.[(triple10)] @1: The cow chases the cow.[(((triple6 triple5) -> rule6) OR ((((triple4) -> rule1) triple5) -> rule6) OR ((((triple8 triple10) -> rule4) triple5) -> rule6))] The cow sees the cow.[(((triple1 triple5) -> rule7))] The lion is rough.[(((triple9 triple10) -> rule2))] The lion visits the lion.[(((triple9) -> rule1))]
The cow chases the lion.
("cow" "chases" "lion" "+")
triple1
The cow is red.
("cow" "is" "red" "+")
triple2
((((triple1 triple5) -> (rule7 % int3)) ((triple6 triple5) -> (rule6 % int2))) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
int3
((((triple1 triple5) -> (rule7 % int4)) ((((triple4) -> (rule1 % int3)) triple5) -> (rule6 % int2))) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow visits the lion.
("cow" "visits" "lion" "+")
int3
The cow sees the cow.
("cow" "sees" "cow" "+")
int4
((((triple1 triple5) -> (rule7 % int4)) ((((triple8 triple10) -> (rule4 % int3)) triple5) -> (rule6 % int2))) -> (rule5 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow visits the lion.
("cow" "visits" "lion" "+")
int3
The cow sees the cow.
("cow" "sees" "cow" "+")
int4
The cow is round.
("cow" "is" "round" "+")
triple3
The cow is young.
("cow" "is" "young" "+")
triple4
The cow sees the lion.
("cow" "sees" "lion" "+")
triple5
The cow visits the lion.
("cow" "visits" "lion" "+")
triple6
((triple4) -> (rule1 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
((triple8 triple10) -> (rule4 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
triple7
The lion is blue.
("lion" "is" "blue" "+")
triple8
The lion is young.
("lion" "is" "young" "+")
triple9
The lion visits the cow.
("lion" "visits" "cow" "+")
triple10
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple6 triple5) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
((((triple4) -> (rule1 % int2)) triple5) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
int2
((((triple8 triple10) -> (rule4 % int2)) triple5) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple1 triple5) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
((triple9 triple10) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple9) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1