Bob is green. Bob is not quiet. Dave is quiet. Quiet people are not white. All quiet people are kind. All red, quiet people are kind. If Dave is quiet then Dave is red. If someone is cold then they are green. Red people are cold.
Bob is green.
("Bob" "is" "green" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Dave is quiet.
("Dave" "is" "quiet" "+")
Quiet people are not white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "-"))
All quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
All red, quiet people are kind.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If Dave is quiet then Dave is red.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "red" "+"))
If someone is cold then they are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
Red people are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Dave is quiet.
True
1
proof
[(triple3)]
("Dave" "is" "quiet" "+")
triple3
Bob is quiet.
False
1
inv-proof
[(triple2)]
("Bob" "is" "quiet" "+")
triple2
Dave is kind.
True
2
proof
[(((triple3) -> rule2) OR ((((triple3) -> rule4) triple3) -> rule3))]
("Dave" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple3) -> (rule4 % int2)) triple3) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
False
2
inv-proof
[(((triple3) -> rule1))]
("Dave" "is" "white" "+")
((triple3) -> (rule1 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is cold.
True
3
proof
[(((((triple3) -> rule4)) -> rule6))]
("Dave" "is" "cold" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not cold.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule6))]
("Dave" "is" "cold" "-")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is green.
True
4
proof
[(((((((triple3) -> rule4)) -> rule6)) -> rule5))]
("Dave" "is" "green" "+")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is not green.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule6)) -> rule5))]
("Dave" "is" "green" "-")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is kind.
Unknown
rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "kind" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is green.[(triple1)] Bob is not quiet.[(triple2)] Dave is quiet.[(triple3)] @1: Dave is kind.[(((triple3) -> rule2) OR ((((triple3) -> rule4) triple3) -> rule3))] Dave is not white.[(((triple3) -> rule1))] Dave is red.[(((triple3) -> rule4))] @2: Dave is cold.[(((((triple3) -> rule4)) -> rule6))] @3: Dave is green.[(((((((triple3) -> rule4)) -> rule6)) -> rule5))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple3) -> (rule4 % int2)) triple3) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not white.
("Dave" "is" "white" "-")
((triple3) -> (rule1 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple3) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3