Fiona is green. Harry is not kind. Harry is red. If someone is red and white then they are not quiet. All quiet people are red. If Harry is red then Harry is white.
Fiona is green.
("Fiona" "is" "green" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is red.
("Harry" "is" "red" "+")
If someone is red and white then they are not quiet.
((("someone" "is" "red" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "-"))
All quiet people are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If Harry is red then Harry is white.
((("Harry" "is" "red" "+")) -> ("Harry" "is" "white" "+"))
Harry is not kind.
True
1
proof
[(triple2)]
("Harry" "is" "kind" "-")
triple2
Harry is kind.
False
1
inv-proof
[(triple2)]
("Harry" "is" "kind" "+")
triple2
Harry is white.
True
2
proof
[(((triple3) -> rule3))]
("Harry" "is" "white" "+")
((triple3) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple3) -> rule3))]
("Harry" "is" "white" "-")
((triple3) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not quiet.
True
4
proof
[(((triple3 ((triple3) -> rule3)) -> rule1))]
("Harry" "is" "quiet" "-")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is quiet.
False
4
inv-proof
[(((triple3 ((triple3) -> rule3)) -> rule1))]
("Harry" "is" "quiet" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "red" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Fiona is green.[(triple1)] Harry is not kind.[(triple2)] Harry is red.[(triple3)] @1: Harry is white.[(((triple3) -> rule3))] @2: Harry is not quiet.[(((triple3 ((triple3) -> rule3)) -> rule1))]
Fiona is green.
("Fiona" "is" "green" "+")
triple1
Harry is not kind.
("Harry" "is" "kind" "-")
triple2
Harry is red.
("Harry" "is" "red" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
((triple3) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not quiet.
("Harry" "is" "quiet" "-")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2