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