The cow is big. The cow is blue. The cow is cold. The cow is green. The cow is nice. If something is blue and big then it is green. Cold things are green. If the cow is blue then the cow is cold. If something is big and cold then it is blue. Nice things are big. Nice things are cold.
The cow is big.
("cow" "is" "big" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is nice.
("cow" "is" "nice" "+")
If something is blue and big then it is green.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
Cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If the cow is blue then the cow is cold.
((("cow" "is" "blue" "+")) -> ("cow" "is" "cold" "+"))
If something is big and cold then it is blue.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
Nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
The cow is blue.
True
1
proof
[(triple2 OR ((triple1 triple3) -> rule4) OR ((triple1 ((triple5) -> rule6)) -> rule4) OR ((((triple5) -> rule5) triple3) -> rule4) OR ((((triple5) -> rule5) ((triple5) -> rule6)) -> rule4))]
("cow" "is" "blue" "+")
triple2
((triple1 triple3) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple1 ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple5) -> (rule5 % int2)) triple3) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
((((triple5) -> (rule5 % int3)) ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is not big.
False
1
inv-proof
[(triple1 OR ((triple5) -> rule5))]
("cow" "is" "big" "-")
triple1
((triple5) -> (rule5 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow does not eat the cow.
Unknown
inv-random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "-")
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 is big.[(triple1 OR ((triple5) -> rule5))] The cow is blue.[(triple2 OR ((triple1 triple3) -> rule4) OR ((triple1 ((triple5) -> rule6)) -> rule4) OR ((((triple5) -> rule5) triple3) -> rule4) OR ((((triple5) -> rule5) ((triple5) -> rule6)) -> rule4))] The cow is cold.[(triple3 OR ((triple2) -> rule3) OR ((triple5) -> rule6))] The cow is green.[(triple4 OR ((triple3) -> rule2) OR ((triple2 triple1) -> rule1) OR ((((triple2) -> rule3)) -> rule2) OR ((((triple5) -> rule6)) -> rule2) OR ((triple2 ((triple5) -> rule5)) -> rule1) OR ((((triple1 triple3) -> rule4) triple1) -> rule1) OR ((((triple1 triple3) -> rule4) ((triple5) -> rule5)) -> rule1) OR ((((triple1 ((triple5) -> rule6)) -> rule4) triple1) -> rule1) OR ((((((triple5) -> rule5) triple3) -> rule4) triple1) -> rule1) OR ((((triple1 ((triple5) -> rule6)) -> rule4) ((triple5) -> rule5)) -> rule1) OR ((((((triple5) -> rule5) triple3) -> rule4) ((triple5) -> rule5)) -> rule1) OR ((((((triple5) -> rule5) ((triple5) -> rule6)) -> rule4) triple1) -> rule1) OR ((((((triple5) -> rule5) ((triple5) -> rule6)) -> rule4) ((triple5) -> rule5)) -> rule1))] The cow is nice.[(triple5)]
The cow is big.
("cow" "is" "big" "+")
triple1
((triple5) -> (rule5 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
triple2
((triple1 triple3) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
((triple1 ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple5) -> (rule5 % int2)) triple3) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
((((triple5) -> (rule5 % int3)) ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
triple3
((triple2) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple5) -> (rule6 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is green.
("cow" "is" "green" "+")
triple4
((triple3) -> (rule2 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
((triple2 triple1) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((((triple5) -> (rule6 % int2))) -> (rule2 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
((triple2 ((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
((((triple1 triple3) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
((((triple1 triple3) -> (rule4 % int3)) ((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3
((((triple1 ((triple5) -> (rule6 % int3))) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
((((((triple5) -> (rule5 % int3)) triple3) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
((((triple1 ((triple5) -> (rule6 % int4))) -> (rule4 % int3)) ((triple5) -> (rule5 % int2))) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
int4
((((((triple5) -> (rule5 % int3)) triple3) -> (rule4 % int2)) ((triple5) -> (rule5 % int3))) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
((((((triple5) -> (rule5 % int4)) ((triple5) -> (rule6 % int3))) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
((((((triple5) -> (rule5 % int4)) ((triple5) -> (rule6 % int3))) -> (rule4 % int2)) ((triple5) -> (rule5 % int4))) -> (rule1 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
The cow is nice.
("cow" "is" "nice" "+")
triple5