Anne is not quiet. Anne is red. Dave is blue. Dave is green. Dave is not quiet. Dave is red. Dave is smart. Gary is green. Gary is quiet. Gary is red. Gary is white. Harry is furry. Harry is green. Harry is quiet. Harry is not smart. Furry, white things are red. If something is white and not furry then it is not blue. All furry things are white.
Anne is not quiet.
("Anne" "is" "quiet" "-")
Anne is red.
("Anne" "is" "red" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
Furry, white things are red.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
If something is white and not furry then it is not blue.
((("something" "is" "white" "+") ("something" "is" "furry" "~")) -> ("something" "is" "blue" "-"))
All furry things are white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
Gary is red.
True
1
proof
[(triple10)]
("Gary" "is" "red" "+")
triple10
Dave is not green.
False
1
inv-proof
[(triple4)]
("Dave" "is" "green" "-")
triple4
Harry is white.
True
2
proof
[(((triple12) -> rule3))]
("Harry" "is" "white" "+")
((triple12) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple12) -> rule3))]
("Harry" "is" "white" "-")
((triple12) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
True
4
proof
[(((triple12 ((triple12) -> rule3)) -> rule1))]
("Harry" "is" "red" "+")
((triple12 ((triple12) -> (rule3 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not red.
False
4
inv-proof
[(((triple12 ((triple12) -> rule3)) -> rule1))]
("Harry" "is" "red" "-")
((triple12 ((triple12) -> (rule3 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "white" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "white" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Anne is not quiet.[(triple1)] Anne is red.[(triple2)] Dave is blue.[(triple3)] Dave is green.[(triple4)] Dave is not quiet.[(triple5)] Dave is red.[(triple6)] Dave is smart.[(triple7)] Gary is green.[(triple8)] Gary is quiet.[(triple9)] Gary is red.[(triple10)] Gary is white.[(triple11)] Harry is furry.[(triple12)] Harry is green.[(triple13)] Harry is not smart.[(triple15)] Harry is quiet.[(triple14)] @1: Harry is white.[(((triple12) -> rule3))] @2: Harry is red.[(((triple12 ((triple12) -> rule3)) -> rule1))]
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Gary is green.
("Gary" "is" "green" "+")
triple8
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
Gary is red.
("Gary" "is" "red" "+")
triple10
Gary is white.
("Gary" "is" "white" "+")
triple11
Harry is furry.
("Harry" "is" "furry" "+")
triple12
Harry is green.
("Harry" "is" "green" "+")
triple13
Harry is not smart.
("Harry" "is" "smart" "-")
triple15
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
((triple12) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple12 ((triple12) -> (rule3 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2