Anne is round. Dave is white. Gary is round. Harry is big. Red things are white. All big things are red. All green, red things are big.
Anne is round.
("Anne" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Red things are white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
All big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
All green, red things are big.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Harry is big.
True
1
proof
[(triple4)]
("Harry" "is" "big" "+")
triple4
Harry is not big.
False
1
inv-proof
[(triple4)]
("Harry" "is" "big" "-")
triple4
Harry is red.
True
2
proof
[(((triple4) -> rule2))]
("Harry" "is" "red" "+")
((triple4) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple4) -> rule2))]
("Harry" "is" "red" "-")
((triple4) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
True
3
proof
[(((((triple4) -> rule2)) -> rule1))]
("Harry" "is" "white" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not white.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule1))]
("Harry" "is" "white" "-")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Gary is not white.
Unknown
inv-rconc
[@3: Gary is white.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule3 <- FAIL)]]
("Gary" "is" "white" "-")
Anne is white.
Unknown
rconc
[@3: Anne is white.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule3 <- FAIL)]]
("Anne" "is" "white" "+")
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "big" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Anne is round.[(triple1)] Dave is white.[(triple2)] Gary is round.[(triple3)] Harry is big.[(triple4)] @1: Harry is red.[(((triple4) -> rule2))] @2: Harry is white.[(((((triple4) -> rule2)) -> rule1))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Harry is red.
("Harry" "is" "red" "+")
((triple4) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2