Dave is big. If something is cold then it is kind. All rough, kind things are not cold. Big things are cold. If Dave is kind and Dave is big then Dave is green. Kind, rough things are blue. If something is green and not rough then it is big.
Dave is big.
("Dave" "is" "big" "+")
If something is cold then it is kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
All rough, kind things are not cold.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "-"))
Big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If Dave is kind and Dave is big then Dave is green.
((("Dave" "is" "kind" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "green" "+"))
Kind, rough things are blue.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If something is green and not rough then it is big.
((("something" "is" "green" "+") ("something" "is" "rough" "~")) -> ("something" "is" "big" "+"))
Dave is big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
Dave is not big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Dave is cold.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("Dave" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Dave" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Dave" "is" "kind" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is green.
True
5
proof
[(((((((triple1) -> rule3)) -> rule1) triple1) -> rule4))]
("Dave" "is" "green" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is not green.
False
5
inv-proof
[(((((((triple1) -> rule3)) -> rule1) triple1) -> rule4))]
("Dave" "is" "green" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Dave is big.[(triple1)] @1: Dave is cold.[(((triple1) -> rule3))] @2: Dave is kind.[(((((triple1) -> rule3)) -> rule1))] @3: Dave is green.[(((((((triple1) -> rule3)) -> rule1) triple1) -> rule4))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3