Fiona is blue. Harry is quiet. Red, blue things are cold. If something is red and blue then it is quiet. If something is blue then it is red.
Fiona is blue.
("Fiona" "is" "blue" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Red, blue things are cold.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If something is red and blue then it is quiet.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If something is blue then it is red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Fiona is blue.
True
1
proof
[(triple1)]
("Fiona" "is" "blue" "+")
triple1
Harry is not quiet.
False
1
inv-proof
[(triple2)]
("Harry" "is" "quiet" "-")
triple2
Fiona is red.
True
2
proof
[(((triple1) -> rule3))]
("Fiona" "is" "red" "+")
((triple1) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not red.
False
2
inv-proof
[(((triple1) -> rule3))]
("Fiona" "is" "red" "-")
((triple1) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is cold.
True
4
proof
[(((((triple1) -> rule3) triple1) -> rule1))]
("Fiona" "is" "cold" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is not quiet.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule2))]
("Fiona" "is" "quiet" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is cold.
Unknown
rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "cold" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Fiona is blue.[(triple1)] Harry is quiet.[(triple2)] @1: Fiona is red.[(((triple1) -> rule3))] @2: Fiona is cold.[(((((triple1) -> rule3) triple1) -> rule1))] Fiona is quiet.[(((((triple1) -> rule3) triple1) -> rule2))]
Fiona is blue.
("Fiona" "is" "blue" "+")
triple1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple2
Fiona is red.
("Fiona" "is" "red" "+")
((triple1) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2