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