Anne is white. Bob is cold. Dave is cold. Harry is cold. White people are red. Green people are kind. If Bob is kind then Bob is red. If Anne is cold and Anne is kind then Anne is blue. If Dave is cold then Dave is white. All white people are big.
Anne is white.
("Anne" "is" "white" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Harry is cold.
("Harry" "is" "cold" "+")
White people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If Bob is kind then Bob is red.
((("Bob" "is" "kind" "+")) -> ("Bob" "is" "red" "+"))
If Anne is cold and Anne is kind then Anne is blue.
((("Anne" "is" "cold" "+") ("Anne" "is" "kind" "+")) -> ("Anne" "is" "blue" "+"))
If Dave is cold then Dave is white.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "white" "+"))
All white people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Anne is white.
True
1
proof
[(triple1)]
("Anne" "is" "white" "+")
triple1
Dave is not cold.
False
1
inv-proof
[(triple3)]
("Dave" "is" "cold" "-")
triple3
Dave is white.
True
2
proof
[(((triple3) -> rule5))]
("Dave" "is" "white" "+")
((triple3) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule6))]
("Anne" "is" "big" "-")
((triple1) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Dave is red.
True
3
proof
[(((((triple3) -> rule5)) -> rule1))]
("Dave" "is" "red" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule6))]
("Dave" "is" "big" "-")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "blue" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "big" "+")
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "red" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Anne is white.[(triple1)] Bob is cold.[(triple2)] Dave is cold.[(triple3)] Harry is cold.[(triple4)] @1: Anne is big.[(((triple1) -> rule6))] Anne is red.[(((triple1) -> rule1))] Dave is white.[(((triple3) -> rule5))] @2: Dave is big.[(((((triple3) -> rule5)) -> rule6))] Dave is red.[(((((triple3) -> rule5)) -> rule1))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple3) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2