Anne is red. Fiona is red. Gary is quiet. Harry is cold. All green things are nice. All furry things are green. All young things are cold. Cold things are red. If something is red then it is green. Green, cold things are quiet.
Anne is red.
("Anne" "is" "red" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is cold.
("Harry" "is" "cold" "+")
All green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
All furry things are green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
All young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
Cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If something is red then it is green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Green, cold things are quiet.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Gary is not quiet.
False
1
inv-proof
[(triple3)]
("Gary" "is" "quiet" "-")
triple3
Harry is red.
True
2
proof
[(((triple4) -> rule4))]
("Harry" "is" "red" "+")
((triple4) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Fiona is not green.
False
2
inv-proof
[(((triple2) -> rule5))]
("Fiona" "is" "green" "-")
((triple2) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Harry is green.
True
3
proof
[(((((triple4) -> rule4)) -> rule5))]
("Harry" "is" "green" "+")
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Fiona is not nice.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule1))]
("Fiona" "is" "nice" "-")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Harry is quiet.
True
5
proof
[(((((((triple4) -> rule4)) -> rule5) triple4) -> rule6))]
("Harry" "is" "quiet" "+")
((((((triple4) -> (rule4 % int3))) -> (rule5 % int2)) triple4) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is not nice.
False
4
inv-proof
[(((((((triple4) -> rule4)) -> rule5)) -> rule1))]
("Harry" "is" "nice" "-")
((((((triple4) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Fiona is not quiet.
Unknown
inv-rconc
[@2: Fiona is quiet.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Anne is quiet.
Unknown
rconc
[@2: Anne is quiet.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Anne" "is" "quiet" "+")
Gary is not red.
Unknown
inv-rconc
[@2: Gary is red.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is green.
Unknown
rconc
[@3: Gary is green.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule3 <- FAIL)]]
("Gary" "is" "green" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is red.[(triple1)] Fiona is red.[(triple2)] Gary is quiet.[(triple3)] Harry is cold.[(triple4)] @1: Anne is green.[(((triple1) -> rule5))] Fiona is green.[(((triple2) -> rule5))] Harry is red.[(((triple4) -> rule4))] @2: Anne is nice.[(((((triple1) -> rule5)) -> rule1))] Fiona is nice.[(((((triple2) -> rule5)) -> rule1))] Harry is green.[(((((triple4) -> rule4)) -> rule5))] @3: Harry is nice.[(((((((triple4) -> rule4)) -> rule5)) -> rule1))] Harry is quiet.[(((((((triple4) -> rule4)) -> rule5) triple4) -> rule6))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Fiona is red.
("Fiona" "is" "red" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple2) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple4) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((((triple4) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
((((((triple4) -> (rule4 % int3))) -> (rule5 % int2)) triple4) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3