Charlie is blue. Dave is red. Fiona is blue. Harry is quiet. All cold things are quiet. If something is green then it is cold. Big, green things are red. If something is green and white then it is red. Cold things are quiet. All red things are green. All cold things are green. If Harry is blue then Harry is red.
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
If something is green then it is cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Big, green things are red.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If something is green and white then it is red.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
Cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
All red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
All cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If Harry is blue then Harry is red.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "red" "+"))
Harry is quiet.
True
1
proof
[(triple4)]
("Harry" "is" "quiet" "+")
triple4
Charlie is not blue.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "blue" "-")
triple1
Dave is green.
True
2
proof
[(((triple2) -> rule6))]
("Dave" "is" "green" "+")
((triple2) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
2
inv-proof
[(((triple2) -> rule6))]
("Dave" "is" "green" "-")
((triple2) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
True
3
proof
[(((((triple2) -> rule6)) -> rule2))]
("Dave" "is" "cold" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not cold.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule2))]
("Dave" "is" "cold" "-")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "red" "-")
Fiona is quiet.
Unknown
rconc
[@4: Fiona is quiet.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule6 <- rule3 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Charlie is not cold.
Unknown
inv-rconc
[@3: Charlie is cold.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule3 <- FAIL)]]
("Charlie" "is" "cold" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Charlie is blue.[(triple1)] Dave is red.[(triple2)] Fiona is blue.[(triple3)] Harry is quiet.[(triple4)] @1: Dave is green.[(((triple2) -> rule6))] @2: Dave is cold.[(((((triple2) -> rule6)) -> rule2))] @3: Dave is quiet.[(((((((triple2) -> rule6)) -> rule2)) -> rule1) OR ((((((triple2) -> rule6)) -> rule2)) -> rule5))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Dave is green.
("Dave" "is" "green" "+")
((triple2) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3