The cow is blue. The lion eats the cow. The lion is big. The lion is green. The lion is rough. The lion sees the cow. The lion visits the cow. If the lion eats the cow and the lion sees the cow then the cow is blue. If someone sees the cow and they visit the cow then they are blue. If someone is green and they see the lion then they eat the lion. If someone is cold and big then they visit the lion. All rough people are cold. If someone is cold and they see the cow then the cow is rough. If someone sees the lion and the lion eats the cow then they eat the cow. If someone sees the lion and the lion visits the cow then the cow is green.
The cow is blue.
("cow" "is" "blue" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
If the lion eats the cow and the lion sees the cow then the cow is blue.
((("lion" "eats" "cow" "+") ("lion" "sees" "cow" "+")) -> ("cow" "is" "blue" "+"))
If someone sees the cow and they visit the cow then they are blue.
((("someone" "sees" "cow" "+") ("someone" "visits" "cow" "+")) -> ("someone" "is" "blue" "+"))
If someone is green and they see the lion then they eat the lion.
((("someone" "is" "green" "+") ("someone" "sees" "lion" "+")) -> ("someone" "eats" "lion" "+"))
If someone is cold and big then they visit the lion.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "visits" "lion" "+"))
All rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold and they see the cow then the cow is rough.
((("someone" "is" "cold" "+") ("someone" "sees" "cow" "+")) -> ("cow" "is" "rough" "+"))
If someone sees the lion and the lion eats the cow then they eat the cow.
((("someone" "sees" "lion" "+") ("lion" "eats" "cow" "+")) -> ("someone" "eats" "cow" "+"))
If someone sees the lion and the lion visits the cow then the cow is green.
((("someone" "sees" "lion" "+") ("lion" "visits" "cow" "+")) -> ("cow" "is" "green" "+"))
The lion eats the cow.
True
1
proof
[(triple2)]
("lion" "eats" "cow" "+")
triple2
The lion is not rough.
False
1
inv-proof
[(triple5)]
("lion" "is" "rough" "-")
triple5
The lion is cold.
True
2
proof
[(((triple5) -> rule5))]
("lion" "is" "cold" "+")
((triple5) -> (rule5 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is not cold.
False
2
inv-proof
[(((triple5) -> rule5))]
("lion" "is" "cold" "-")
((triple5) -> (rule5 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion visits the lion.
True
4
proof
[(((((triple5) -> rule5) triple3) -> rule4))]
("lion" "visits" "lion" "+")
((((triple5) -> (rule5 % int2)) triple3) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The cow is not rough.
False
4
inv-proof
[(((((triple5) -> rule5) triple6) -> rule6))]
("cow" "is" "rough" "-")
((((triple5) -> (rule5 % int2)) triple6) -> (rule6 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The cow is cold.
True
5
proof
[(((((((triple5) -> rule5) triple6) -> rule6)) -> rule5))]
("cow" "is" "cold" "+")
((((((triple5) -> (rule5 % int3)) triple6) -> (rule6 % int2))) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The cow is not cold.
False
5
inv-proof
[(((((((triple5) -> rule5) triple6) -> rule6)) -> rule5))]
("cow" "is" "cold" "-")
((((((triple5) -> (rule5 % int3)) triple6) -> (rule6 % int2))) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The cow does not eat the cow.
Unknown
inv-rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "eats" "cow" "-")
The lion eats the lion.
Unknown
rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "eats" "lion" "+")
The cow is not green.
Unknown
inv-rconc
[@1: The cow is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "is" "green" "-")
The cow eats the lion.
Unknown
rconc
[@1: The cow eats the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "eats" "lion" "+")
The cow does not see the lion.
Unknown
inv-random
[@0: The cow sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "lion" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "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 is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
@0: The cow is blue.[(triple1 OR ((triple2 triple6) -> rule1))] The lion eats the cow.[(triple2)] The lion is big.[(triple3)] The lion is green.[(triple4)] The lion is rough.[(triple5)] The lion sees the cow.[(triple6)] The lion visits the cow.[(triple7)] @1: The lion is blue.[(((triple6 triple7) -> rule2))] The lion is cold.[(((triple5) -> rule5))] @2: The cow is rough.[(((((triple5) -> rule5) triple6) -> rule6))] The lion visits the lion.[(((((triple5) -> rule5) triple3) -> rule4))] @3: The cow is cold.[(((((((triple5) -> rule5) triple6) -> rule6)) -> rule5))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
((triple2 triple6) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
triple2
The lion is big.
("lion" "is" "big" "+")
triple3
The lion is green.
("lion" "is" "green" "+")
triple4
The lion is rough.
("lion" "is" "rough" "+")
triple5
The lion sees the cow.
("lion" "sees" "cow" "+")
triple6
The lion visits the cow.
("lion" "visits" "cow" "+")
triple7
The lion is blue.
("lion" "is" "blue" "+")
((triple6 triple7) -> (rule2 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
((triple5) -> (rule5 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
((((triple5) -> (rule5 % int2)) triple6) -> (rule6 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion visits the lion.
("lion" "visits" "lion" "+")
((((triple5) -> (rule5 % int2)) triple3) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
((((((triple5) -> (rule5 % int3)) triple6) -> (rule6 % int2))) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3