The cow does not chase the lion. The cow does not eat the lion. The cow is red. The cow is round. The cow visits the lion. The lion chases the cow. The lion eats the cow. The lion is big. The lion is red. The lion visits the cow. If something visits the cow and the cow does not eat the lion then the lion is round. If something eats the lion then the lion is not round. If something chases the cow and it visits the lion then the cow is young. If something is big then it visits the lion. If something chases the lion and the lion chases the cow then it does not chase the cow. If something chases the lion and the lion eats the cow then the lion does not visit the cow. If something chases the cow and it visits the lion then the cow is nice. All young things are big.
The cow does not chase the lion.
("cow" "chases" "lion" "-")
The cow does not eat the lion.
("cow" "eats" "lion" "-")
The cow is red.
("cow" "is" "red" "+")
The cow is round.
("cow" "is" "round" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is red.
("lion" "is" "red" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
If something visits the cow and the cow does not eat the lion then the lion is round.
((("something" "visits" "cow" "+") ("cow" "eats" "lion" "~")) -> ("lion" "is" "round" "+"))
If something eats the lion then the lion is not round.
((("something" "eats" "lion" "+")) -> ("lion" "is" "round" "-"))
If something chases the cow and it visits the lion then the cow is young.
((("something" "chases" "cow" "+") ("something" "visits" "lion" "+")) -> ("cow" "is" "young" "+"))
If something is big then it visits the lion.
((("something" "is" "big" "+")) -> ("something" "visits" "lion" "+"))
If something chases the lion and the lion chases the cow then it does not chase the cow.
((("something" "chases" "lion" "+") ("lion" "chases" "cow" "+")) -> ("something" "chases" "cow" "-"))
If something chases the lion and the lion eats the cow then the lion does not visit the cow.
((("something" "chases" "lion" "+") ("lion" "eats" "cow" "+")) -> ("lion" "visits" "cow" "-"))
If something chases the cow and it visits the lion then the cow is nice.
((("something" "chases" "cow" "+") ("something" "visits" "lion" "+")) -> ("cow" "is" "nice" "+"))
All young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
The lion chases the cow.
True
1
proof
[(triple6)]
("lion" "chases" "cow" "+")
triple6
The cow eats the lion.
False
1
inv-proof
[(triple2)]
("cow" "eats" "lion" "+")
triple2
The lion visits the lion.
True
2
proof
[(((triple8) -> rule4))]
("lion" "visits" "lion" "+")
((triple8) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion does not visit the lion.
False
2
inv-proof
[(((triple8) -> rule4))]
("lion" "visits" "lion" "-")
((triple8) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The cow is young.
True
4
proof
[(((triple6 ((triple8) -> rule4)) -> rule3))]
("cow" "is" "young" "+")
((triple6 ((triple8) -> (rule4 % int2))) -> (rule3 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The cow is not nice.
False
4
inv-proof
[(((triple6 ((triple8) -> rule4)) -> rule7))]
("cow" "is" "nice" "-")
((triple6 ((triple8) -> (rule4 % int2))) -> (rule7 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The cow is big.
True
5
proof
[(((((triple6 ((triple8) -> rule4)) -> rule3)) -> rule8))]
("cow" "is" "big" "+")
((((triple6 ((triple8) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The lion visits the lion.
("lion" "visits" "lion" "+")
int3
The cow is not big.
False
5
inv-proof
[(((((triple6 ((triple8) -> rule4)) -> rule3)) -> rule8))]
("cow" "is" "big" "-")
((((triple6 ((triple8) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The lion visits the lion.
("lion" "visits" "lion" "+")
int3
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow does not chase the lion.[(triple1)] The cow does not eat the lion.[(triple2)] The cow is red.[(triple3)] The cow is round.[(triple4)] The cow visits the lion.[(triple5 OR ((((((triple6 ((triple8) -> rule4)) -> rule3)) -> rule8)) -> rule4))] The lion chases the cow.[(triple6)] The lion eats the cow.[(triple7)] The lion is big.[(triple8)] The lion is red.[(triple9)] The lion visits the cow.[(triple10)] @1: The lion is round.[(((triple10 triple2) -> rule1))] The lion visits the lion.[(((triple8) -> rule4))] @2: The cow is nice.[(((triple6 ((triple8) -> rule4)) -> rule7))] The cow is young.[(((triple6 ((triple8) -> rule4)) -> rule3))] @3: The cow is big.[(((((triple6 ((triple8) -> rule4)) -> rule3)) -> rule8))]
The cow does not chase the lion.
("cow" "chases" "lion" "-")
triple1
The cow does not eat the lion.
("cow" "eats" "lion" "-")
triple2
The cow is red.
("cow" "is" "red" "+")
triple3
The cow is round.
("cow" "is" "round" "+")
triple4
The cow visits the lion.
("cow" "visits" "lion" "+")
triple5
((((((triple6 ((triple8) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is young.
("cow" "is" "young" "+")
int3
The lion visits the lion.
("lion" "visits" "lion" "+")
int4
The lion chases the cow.
("lion" "chases" "cow" "+")
triple6
The lion eats the cow.
("lion" "eats" "cow" "+")
triple7
The lion is big.
("lion" "is" "big" "+")
triple8
The lion is red.
("lion" "is" "red" "+")
triple9
The lion visits the cow.
("lion" "visits" "cow" "+")
triple10
The lion is round.
("lion" "is" "round" "+")
((triple10 triple2) -> (rule1 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple8) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
((triple6 ((triple8) -> (rule4 % int2))) -> (rule7 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The cow is young.
("cow" "is" "young" "+")
((triple6 ((triple8) -> (rule4 % int2))) -> (rule3 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The cow is big.
("cow" "is" "big" "+")
((((triple6 ((triple8) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The lion visits the lion.
("lion" "visits" "lion" "+")
int3