The cow is young. The lion is cold. If something needs the lion then the lion visits the cow. If something needs the lion and it eats the lion then it is big. If something eats the cow then it is big. If something needs the cow and it needs the lion then the cow does not eat the lion. If something needs the cow and it visits the lion then the cow is big. If something needs the lion then the lion eats the cow. If something is young then it needs the lion. If something needs the cow and it visits the lion then it needs the lion.
The cow is young.
("cow" "is" "young" "+")
The lion is cold.
("lion" "is" "cold" "+")
If something needs the lion then the lion visits the cow.
((("something" "needs" "lion" "+")) -> ("lion" "visits" "cow" "+"))
If something needs the lion and it eats the lion then it is big.
((("something" "needs" "lion" "+") ("something" "eats" "lion" "+")) -> ("something" "is" "big" "+"))
If something eats the cow then it is big.
((("something" "eats" "cow" "+")) -> ("something" "is" "big" "+"))
If something needs the cow and it needs the lion then the cow does not eat the lion.
((("something" "needs" "cow" "+") ("something" "needs" "lion" "+")) -> ("cow" "eats" "lion" "-"))
If something needs the cow and it visits the lion then the cow is big.
((("something" "needs" "cow" "+") ("something" "visits" "lion" "+")) -> ("cow" "is" "big" "+"))
If something needs the lion then the lion eats the cow.
((("something" "needs" "lion" "+")) -> ("lion" "eats" "cow" "+"))
If something is young then it needs the lion.
((("something" "is" "young" "+")) -> ("something" "needs" "lion" "+"))
If something needs the cow and it visits the lion then it needs the lion.
((("something" "needs" "cow" "+") ("something" "visits" "lion" "+")) -> ("something" "needs" "lion" "+"))
The lion is cold.
True
1
proof
[(triple2)]
("lion" "is" "cold" "+")
triple2
The lion is not cold.
False
1
inv-proof
[(triple2)]
("lion" "is" "cold" "-")
triple2
The cow needs the lion.
True
2
proof
[(((triple1) -> rule7))]
("cow" "needs" "lion" "+")
((triple1) -> (rule7 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow does not need the lion.
False
2
inv-proof
[(((triple1) -> rule7))]
("cow" "needs" "lion" "-")
((triple1) -> (rule7 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The lion visits the cow.
True
3
proof
[(((((triple1) -> rule7)) -> rule1))]
("lion" "visits" "cow" "+")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The cow needs the lion.
("cow" "needs" "lion" "+")
int2
The lion does not eat the cow.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule6))]
("lion" "eats" "cow" "-")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The cow needs the lion.
("cow" "needs" "lion" "+")
int2
The lion is big.
True
4
proof
[(((((((triple1) -> rule7)) -> rule6)) -> rule3))]
("lion" "is" "big" "+")
((((((triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The cow needs the lion.
("cow" "needs" "lion" "+")
int3
The lion is not big.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule6)) -> rule3))]
("lion" "is" "big" "-")
((((((triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The cow needs the lion.
("cow" "needs" "lion" "+")
int3
The cow is not big.
Unknown
inv-rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "big" "-")
The lion needs the lion.
Unknown
rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "needs" "lion" "+")
The cow does not eat the lion.
Unknown
inv-random
[@0: The cow eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "lion" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The cow is not cold.
Unknown
inv-random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The lion does not need the cow.
Unknown
inv-random
[@0: The lion needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cow" "-")
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 is young.[(triple1)] The lion is cold.[(triple2)] @1: The cow needs the lion.[(((triple1) -> rule7))] @2: The lion eats the cow.[(((((triple1) -> rule7)) -> rule6))] The lion visits the cow.[(((((triple1) -> rule7)) -> rule1))] @3: The lion is big.[(((((((triple1) -> rule7)) -> rule6)) -> rule3))]
The cow is young.
("cow" "is" "young" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The cow needs the lion.
("cow" "needs" "lion" "+")
((triple1) -> (rule7 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The cow needs the lion.
("cow" "needs" "lion" "+")
int2
The lion visits the cow.
("lion" "visits" "cow" "+")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
The lion visits the cow.
("lion" "visits" "cow" "+")
int1
The cow needs the lion.
("cow" "needs" "lion" "+")
int2
The lion is big.
("lion" "is" "big" "+")
((((((triple1) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The cow needs the lion.
("cow" "needs" "lion" "+")
int3