Dave is green. Dave is not red. Dave is round. Harry is blue. Harry is not furry. Harry is green. Harry is white. If Dave is not white and Dave is not young then Dave is furry. If someone is round and white then they are red. If someone is blue and not young then they are round. If someone is red and not white then they are blue. If Harry is blue then Harry is round. All young people are green.
Dave is green.
("Dave" "is" "green" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is round.
("Dave" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is not furry.
("Harry" "is" "furry" "-")
Harry is green.
("Harry" "is" "green" "+")
Harry is white.
("Harry" "is" "white" "+")
If Dave is not white and Dave is not young then Dave is furry.
((("Dave" "is" "white" "~") ("Dave" "is" "young" "~")) -> ("Dave" "is" "furry" "+"))
If someone is round and white then they are red.
((("someone" "is" "round" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
If someone is blue and not young then they are round.
((("someone" "is" "blue" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "round" "+"))
If someone is red and not white then they are blue.
((("someone" "is" "red" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "blue" "+"))
If Harry is blue then Harry is round.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "round" "+"))
All young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Dave is round.
True
1
proof
[(triple3)]
("Dave" "is" "round" "+")
triple3
Harry is not green.
False
1
inv-proof
[(triple6)]
("Harry" "is" "green" "-")
triple6
Harry is round.
True
2
proof
[(((triple4) -> rule5))]
("Harry" "is" "round" "+")
((triple4) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple4) -> rule5))]
("Harry" "is" "round" "-")
((triple4) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
True
4
proof
[(((((triple4) -> rule5) triple7) -> rule2))]
("Harry" "is" "red" "+")
((((triple4) -> (rule5 % int2)) triple7) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not red.
False
4
inv-proof
[(((((triple4) -> rule5) triple7) -> rule2))]
("Harry" "is" "red" "-")
((((triple4) -> (rule5 % int2)) triple7) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is blue.
Unknown
rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "blue" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Dave is green.[(triple1)] Dave is not red.[(triple2)] Dave is round.[(triple3)] Harry is blue.[(triple4)] Harry is green.[(triple6)] Harry is not furry.[(triple5)] Harry is white.[(triple7)] @1: Harry is round.[(((triple4) -> rule5))] @2: Harry is red.[(((((triple4) -> rule5) triple7) -> rule2))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is not red.
("Dave" "is" "red" "-")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Harry is green.
("Harry" "is" "green" "+")
triple6
Harry is not furry.
("Harry" "is" "furry" "-")
triple5
Harry is white.
("Harry" "is" "white" "+")
triple7
Harry is round.
("Harry" "is" "round" "+")
((triple4) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((((triple4) -> (rule5 % int2)) triple7) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2