The cow is blue. The cow visits the lion. The lion does not need the cow. If something is nice then it needs the lion. All big things are nice. If something is red then it does not eat the cow. If the cow visits the lion then the cow needs the lion. If something eats the lion and the lion is not big then it visits the lion. If something eats the lion then the lion is green. If the cow needs the lion then the cow eats the lion. If the cow is not nice and the cow is not red then the cow does not eat the lion.
The cow is blue.
("cow" "is" "blue" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion does not need the cow.
("lion" "needs" "cow" "-")
If something is nice then it needs the lion.
((("something" "is" "nice" "+")) -> ("something" "needs" "lion" "+"))
All big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If something is red then it does not eat the cow.
((("something" "is" "red" "+")) -> ("something" "eats" "cow" "-"))
If the cow visits the lion then the cow needs the lion.
((("cow" "visits" "lion" "+")) -> ("cow" "needs" "lion" "+"))
If something eats the lion and the lion is not big then it visits the lion.
((("something" "eats" "lion" "+") ("lion" "is" "big" "~")) -> ("something" "visits" "lion" "+"))
If something eats the lion then the lion is green.
((("something" "eats" "lion" "+")) -> ("lion" "is" "green" "+"))
If the cow needs the lion then the cow eats the lion.
((("cow" "needs" "lion" "+")) -> ("cow" "eats" "lion" "+"))
If the cow is not nice and the cow is not red then the cow does not eat the lion.
((("cow" "is" "nice" "~") ("cow" "is" "red" "~")) -> ("cow" "eats" "lion" "-"))
The cow is blue.
True
1
proof
[(triple1)]
("cow" "is" "blue" "+")
triple1
The cow is not blue.
False
1
inv-proof
[(triple1)]
("cow" "is" "blue" "-")
triple1
The cow needs the lion.
True
2
proof
[(((triple2) -> rule4))]
("cow" "needs" "lion" "+")
((triple2) -> (rule4 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow does not need the lion.
False
2
inv-proof
[(((triple2) -> rule4))]
("cow" "needs" "lion" "-")
((triple2) -> (rule4 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow eats the lion.
True
3
proof
[(((((triple2) -> rule4)) -> rule7))]
("cow" "eats" "lion" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow needs the lion.
("cow" "needs" "lion" "+")
int2
The cow does not eat the lion.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule7))]
("cow" "eats" "lion" "-")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow needs the lion.
("cow" "needs" "lion" "+")
int2
The lion is green.
True
4
proof
[(((((((triple2) -> rule4)) -> rule7)) -> rule6))]
("lion" "is" "green" "+")
((((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The cow needs the lion.
("cow" "needs" "lion" "+")
int3
The lion is not green.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule7)) -> rule6))]
("lion" "is" "green" "-")
((((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The cow needs the lion.
("cow" "needs" "lion" "+")
int3
The cow is not nice.
Unknown
inv-rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "nice" "-")
The lion visits the lion.
Unknown
rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "visits" "lion" "+")
The lion does not need the lion.
Unknown
inv-rconc
[@2: The lion needs the lion.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("lion" "needs" "lion" "-")
The lion is nice.
Unknown
rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "nice" "+")
The lion is not big.
Unknown
inv-random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow is blue.[(triple1)] The cow visits the lion.[(triple2)] The lion does not need the cow.[(triple3)] @1: The cow needs the lion.[(((triple2) -> rule4))] @2: The cow eats the lion.[(((((triple2) -> rule4)) -> rule7))] @3: The lion is green.[(((((((triple2) -> rule4)) -> rule7)) -> rule6))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The cow visits the lion.
("cow" "visits" "lion" "+")
triple2
The lion does not need the cow.
("lion" "needs" "cow" "-")
triple3
The cow needs the lion.
("cow" "needs" "lion" "+")
((triple2) -> (rule4 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow needs the lion.
("cow" "needs" "lion" "+")
int2
The lion is green.
("lion" "is" "green" "+")
((((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The cow needs the lion.
("cow" "needs" "lion" "+")
int3