Charlie is green. Fiona is red. Green things are blue. Quiet things are blue. If Charlie is blue then Charlie is quiet. All green, red things are kind. Blue, red things are quiet. If something is kind and green then it is furry. If something is furry and green then it is cold. If something is quiet then it is red.
Charlie is green.
("Charlie" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If Charlie is blue then Charlie is quiet.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "quiet" "+"))
All green, red things are kind.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Blue, red things are quiet.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If something is kind and green then it is furry.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
If something is furry and green then it is cold.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something is quiet then it is red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
Charlie is green.
True
1
proof
[(triple1)]
("Charlie" "is" "green" "+")
triple1
Charlie is not green.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "green" "-")
triple1
Charlie is blue.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not blue.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "blue" "-")
((triple1) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not quiet.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Charlie" "is" "quiet" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
True
4
proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule8))]
("Charlie" "is" "red" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is not red.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule8))]
("Charlie" "is" "red" "-")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is blue.
Unknown
rconc
[@3: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- rule5 <- rule1 <- FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "furry" "-")
Fiona is quiet.
Unknown
rconc
[@2: Fiona is quiet.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Charlie is green.[(triple1)] Fiona is red.[(triple2)] @1: Charlie is blue.[(((triple1) -> rule1))] @2: Charlie is quiet.[(((((triple1) -> rule1)) -> rule3))] @3: Charlie is red.[(((((((triple1) -> rule1)) -> rule3)) -> rule8))] @4: Charlie is kind.[(((triple1 ((((((triple1) -> rule1)) -> rule3)) -> rule8)) -> rule4))] @5: Charlie is furry.[(((((triple1 ((((((triple1) -> rule1)) -> rule3)) -> rule8)) -> rule4) triple1) -> rule6))] @6: Charlie is cold.[(((((((triple1 ((((((triple1) -> rule1)) -> rule3)) -> rule8)) -> rule4) triple1) -> rule6) triple1) -> rule7))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Fiona is red.
("Fiona" "is" "red" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1 ((((((triple1) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple1 ((((((triple1) -> (rule1 % int5))) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) triple1) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is blue.
("Charlie" "is" "blue" "+")
int5
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple1 ((((((triple1) -> (rule1 % int6))) -> (rule3 % int5))) -> (rule8 % int4))) -> (rule4 % int3)) triple1) -> (rule6 % int2)) triple1) -> (rule7 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int5
Charlie is blue.
("Charlie" "is" "blue" "+")
int6