Dave is rough. If someone is red and not blue then they are green. If Dave is white then Dave is red. If Dave is red then Dave is not cold. All rough people are white. Green, kind people are not cold. If someone is rough and not red then they are not kind.
Dave is rough.
("Dave" "is" "rough" "+")
If someone is red and not blue then they are green.
((("someone" "is" "red" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "green" "+"))
If Dave is white then Dave is red.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "red" "+"))
If Dave is red then Dave is not cold.
((("Dave" "is" "red" "+")) -> ("Dave" "is" "cold" "-"))
All rough people are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
Green, kind people are not cold.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "-"))
If someone is rough and not red then they are not kind.
((("someone" "is" "rough" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "kind" "-"))
Dave is rough.
True
1
proof
[(triple1)]
("Dave" "is" "rough" "+")
triple1
Dave is not rough.
False
1
inv-proof
[(triple1)]
("Dave" "is" "rough" "-")
triple1
Dave is white.
True
2
proof
[(((triple1) -> rule4))]
("Dave" "is" "white" "+")
((triple1) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple1) -> rule4))]
("Dave" "is" "white" "-")
((triple1) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
True
3
proof
[(((((triple1) -> rule4)) -> rule2))]
("Dave" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not red.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2))]
("Dave" "is" "red" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not cold.
True
4
proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule3))]
("Dave" "is" "cold" "-")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is cold.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule3))]
("Dave" "is" "cold" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Dave is rough.[(triple1)] @1: Dave is white.[(((triple1) -> rule4))] @2: Dave is red.[(((((triple1) -> rule4)) -> rule2))] @3: Dave is not cold.[(((((((triple1) -> rule4)) -> rule2)) -> rule3))]
Dave is rough.
("Dave" "is" "rough" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
((triple1) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not cold.
("Dave" "is" "cold" "-")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3