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