The cow eats the lion. The cow is round. The cow sees the lion. The lion eats the cow. The lion is green. The lion sees the cow. The lion visits the cow. Rough things are green. If something sees the lion and the lion visits the cow then it eats the cow. If something sees the lion and it visits the cow then the lion sees the cow. If the lion sees the cow and the cow sees the lion then the lion is young. If something eats the cow and the cow is round then it visits the cow. If the lion is rough then the lion sees the cow. If something visits the cow then it is green. If the cow visits the lion then the cow sees the lion.
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow is round.
("cow" "is" "round" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion is green.
("lion" "is" "green" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
Rough things are green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something sees the lion and the lion visits the cow then it eats the cow.
((("something" "sees" "lion" "+") ("lion" "visits" "cow" "+")) -> ("something" "eats" "cow" "+"))
If something sees the lion and it visits the cow then the lion sees the cow.
((("something" "sees" "lion" "+") ("something" "visits" "cow" "+")) -> ("lion" "sees" "cow" "+"))
If the lion sees the cow and the cow sees the lion then the lion is young.
((("lion" "sees" "cow" "+") ("cow" "sees" "lion" "+")) -> ("lion" "is" "young" "+"))
If something eats the cow and the cow is round then it visits the cow.
((("something" "eats" "cow" "+") ("cow" "is" "round" "+")) -> ("something" "visits" "cow" "+"))
If the lion is rough then the lion sees the cow.
((("lion" "is" "rough" "+")) -> ("lion" "sees" "cow" "+"))
If something visits the cow then it is green.
((("something" "visits" "cow" "+")) -> ("something" "is" "green" "+"))
If the cow visits the lion then the cow sees the lion.
((("cow" "visits" "lion" "+")) -> ("cow" "sees" "lion" "+"))
The cow eats the lion.
True
1
proof
[(triple1)]
("cow" "eats" "lion" "+")
triple1
The lion is not green.
False
1
inv-proof
[(triple5 OR ((triple7) -> rule7) OR ((((triple4 triple2) -> rule5)) -> rule7))]
("lion" "is" "green" "-")
triple5
((triple7) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
((((triple4 triple2) -> (rule5 % int2))) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The cow eats the cow.
True
3
proof
[(((triple3 triple7) -> rule2) OR ((triple3 ((triple4 triple2) -> rule5)) -> rule2))]
("cow" "eats" "cow" "+")
((triple3 triple7) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
((triple3 ((triple4 triple2) -> (rule5 % int2))) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The lion is not young.
False
3
inv-proof
[(((triple6 triple3) -> rule4) OR ((((triple3 ((((triple3 triple7) -> rule2) triple2) -> rule5)) -> rule3) triple3) -> rule4) OR ((((triple3 ((((triple3 ((triple4 triple2) -> rule5)) -> rule2) triple2) -> rule5)) -> rule3) triple3) -> rule4))]
("lion" "is" "young" "-")
((triple6 triple3) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((((triple3 ((((triple3 triple7) -> (rule2 % int4)) triple2) -> (rule5 % int3))) -> (rule3 % int2)) triple3) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow eats the cow.
("cow" "eats" "cow" "+")
int4
((((triple3 ((((triple3 ((triple4 triple2) -> (rule5 % int5))) -> (rule2 % int4)) triple2) -> (rule5 % int3))) -> (rule3 % int2)) triple3) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow eats the cow.
("cow" "eats" "cow" "+")
int4
The lion visits the cow.
("lion" "visits" "cow" "+")
int5
The cow visits the cow.
True
5
proof
[(((((triple3 triple7) -> rule2) triple2) -> rule5) OR ((((triple3 ((triple4 triple2) -> rule5)) -> rule2) triple2) -> rule5))]
("cow" "visits" "cow" "+")
((((triple3 triple7) -> (rule2 % int2)) triple2) -> (rule5 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
((((triple3 ((triple4 triple2) -> (rule5 % int3))) -> (rule2 % int2)) triple2) -> (rule5 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The lion visits the cow.
("lion" "visits" "cow" "+")
int3
The cow does not visit the cow.
False
5
inv-proof
[(((((triple3 triple7) -> rule2) triple2) -> rule5) OR ((((triple3 ((triple4 triple2) -> rule5)) -> rule2) triple2) -> rule5))]
("cow" "visits" "cow" "-")
((((triple3 triple7) -> (rule2 % int2)) triple2) -> (rule5 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
((((triple3 ((triple4 triple2) -> (rule5 % int3))) -> (rule2 % int2)) triple2) -> (rule5 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The lion visits the cow.
("lion" "visits" "cow" "+")
int3
The cow is green.
True
6
proof
[(((((((triple3 triple7) -> rule2) triple2) -> rule5)) -> rule7) OR ((((((triple3 ((triple4 triple2) -> rule5)) -> rule2) triple2) -> rule5)) -> rule7))]
("cow" "is" "green" "+")
((((((triple3 triple7) -> (rule2 % int3)) triple2) -> (rule5 % int2))) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
((((((triple3 ((triple4 triple2) -> (rule5 % int4))) -> (rule2 % int3)) triple2) -> (rule5 % int2))) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The lion visits the cow.
("lion" "visits" "cow" "+")
int4
The cow is not green.
False
6
inv-proof
[(((((((triple3 triple7) -> rule2) triple2) -> rule5)) -> rule7) OR ((((((triple3 ((triple4 triple2) -> rule5)) -> rule2) triple2) -> rule5)) -> rule7))]
("cow" "is" "green" "-")
((((((triple3 triple7) -> (rule2 % int3)) triple2) -> (rule5 % int2))) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
((((((triple3 ((triple4 triple2) -> (rule5 % int4))) -> (rule2 % int3)) triple2) -> (rule5 % int2))) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The lion visits the cow.
("lion" "visits" "cow" "+")
int4
The lion is not rough.
Unknown
inv-random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The lion is not round.
Unknown
inv-random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The cow does not visit the lion.
Unknown
inv-random
[@0: The cow visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "lion" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cow eats the lion.[(triple1)] The cow is round.[(triple2)] The cow sees the lion.[(triple3)] The lion eats the cow.[(triple4)] The lion is green.[(triple5 OR ((triple7) -> rule7) OR ((((triple4 triple2) -> rule5)) -> rule7))] The lion sees the cow.[(triple6 OR ((triple3 ((((triple3 triple7) -> rule2) triple2) -> rule5)) -> rule3) OR ((triple3 ((((triple3 ((triple4 triple2) -> rule5)) -> rule2) triple2) -> rule5)) -> rule3))] The lion visits the cow.[(triple7 OR ((triple4 triple2) -> rule5))] @1: The cow eats the cow.[(((triple3 triple7) -> rule2) OR ((triple3 ((triple4 triple2) -> rule5)) -> rule2))] The lion is young.[(((triple6 triple3) -> rule4) OR ((((triple3 ((((triple3 triple7) -> rule2) triple2) -> rule5)) -> rule3) triple3) -> rule4) OR ((((triple3 ((((triple3 ((triple4 triple2) -> rule5)) -> rule2) triple2) -> rule5)) -> rule3) triple3) -> rule4))] @2: The cow visits the cow.[(((((triple3 triple7) -> rule2) triple2) -> rule5) OR ((((triple3 ((triple4 triple2) -> rule5)) -> rule2) triple2) -> rule5))] @3: The cow is green.[(((((((triple3 triple7) -> rule2) triple2) -> rule5)) -> rule7) OR ((((((triple3 ((triple4 triple2) -> rule5)) -> rule2) triple2) -> rule5)) -> rule7))]
The cow eats the lion.
("cow" "eats" "lion" "+")
triple1
The cow is round.
("cow" "is" "round" "+")
triple2
The cow sees the lion.
("cow" "sees" "lion" "+")
triple3
The lion eats the cow.
("lion" "eats" "cow" "+")
triple4
The lion is green.
("lion" "is" "green" "+")
triple5
((triple7) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
((((triple4 triple2) -> (rule5 % int2))) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The lion sees the cow.
("lion" "sees" "cow" "+")
triple6
((triple3 ((((triple3 triple7) -> (rule2 % int3)) triple2) -> (rule5 % int2))) -> (rule3 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
((triple3 ((((triple3 ((triple4 triple2) -> (rule5 % int4))) -> (rule2 % int3)) triple2) -> (rule5 % int2))) -> (rule3 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The lion visits the cow.
("lion" "visits" "cow" "+")
int4
The lion visits the cow.
("lion" "visits" "cow" "+")
triple7
((triple4 triple2) -> (rule5 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
((triple3 triple7) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
((triple3 ((triple4 triple2) -> (rule5 % int2))) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The lion visits the cow.
("lion" "visits" "cow" "+")
int2
The lion is young.
("lion" "is" "young" "+")
((triple6 triple3) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((((triple3 ((((triple3 triple7) -> (rule2 % int4)) triple2) -> (rule5 % int3))) -> (rule3 % int2)) triple3) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow eats the cow.
("cow" "eats" "cow" "+")
int4
((((triple3 ((((triple3 ((triple4 triple2) -> (rule5 % int5))) -> (rule2 % int4)) triple2) -> (rule5 % int3))) -> (rule3 % int2)) triple3) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3
The cow eats the cow.
("cow" "eats" "cow" "+")
int4
The lion visits the cow.
("lion" "visits" "cow" "+")
int5
The cow visits the cow.
("cow" "visits" "cow" "+")
((((triple3 triple7) -> (rule2 % int2)) triple2) -> (rule5 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
((((triple3 ((triple4 triple2) -> (rule5 % int3))) -> (rule2 % int2)) triple2) -> (rule5 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The lion visits the cow.
("lion" "visits" "cow" "+")
int3
The cow is green.
("cow" "is" "green" "+")
((((((triple3 triple7) -> (rule2 % int3)) triple2) -> (rule5 % int2))) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
((((((triple3 ((triple4 triple2) -> (rule5 % int4))) -> (rule2 % int3)) triple2) -> (rule5 % int2))) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The lion visits the cow.
("lion" "visits" "cow" "+")
int4