Bob is young. Dave is white. Gary is smart. Harry is round. If something is round then it is blue. Young, white things are smart. Red things are round. If something is smart then it is red. All red, blue things are white. If Harry is cold and Harry is blue then Harry is red.
Bob is young.
("Bob" "is" "young" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is round then it is blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Young, white things are smart.
((("something" "is" "young" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
Red things are round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
If something is smart then it is red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
All red, blue things are white.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
If Harry is cold and Harry is blue then Harry is red.
((("Harry" "is" "cold" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "red" "+"))
Dave is white.
True
1
proof
[(triple2)]
("Dave" "is" "white" "+")
triple2
Harry is not round.
False
1
inv-proof
[(triple4)]
("Harry" "is" "round" "-")
triple4
Gary is red.
True
2
proof
[(((triple3) -> rule4))]
("Gary" "is" "red" "+")
((triple3) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not red.
False
2
inv-proof
[(((triple3) -> rule4))]
("Gary" "is" "red" "-")
((triple3) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
True
3
proof
[(((((triple3) -> rule4)) -> rule3))]
("Gary" "is" "round" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not round.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule3))]
("Gary" "is" "round" "-")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is blue.
True
4
proof
[(((((((triple3) -> rule4)) -> rule3)) -> rule1))]
("Gary" "is" "blue" "+")
((((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is not blue.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule3)) -> rule1))]
("Gary" "is" "blue" "-")
((((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Dave is not red.
Unknown
inv-rconc
[@2: Dave is red.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Dave" "is" "red" "-")
Harry is white.
Unknown
rconc
[@3: Harry is white.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule2 <- FAIL)]]
("Harry" "is" "white" "+")
Bob is not round.
Unknown
inv-rconc
[@4: Bob is round.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule2 <- rule5 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is red.
Unknown
rconc
[@3: Bob is red.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule5 <- FAIL)]]
("Bob" "is" "red" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is young.[(triple1)] Dave is white.[(triple2)] Gary is smart.[(triple3)] Harry is round.[(triple4)] @1: Gary is red.[(((triple3) -> rule4))] Harry is blue.[(((triple4) -> rule1))] @2: Gary is round.[(((((triple3) -> rule4)) -> rule3))] @3: Gary is blue.[(((((((triple3) -> rule4)) -> rule3)) -> rule1))] @4: Gary is white.[(((((triple3) -> rule4) ((((((triple3) -> rule4)) -> rule3)) -> rule1)) -> rule5))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
((triple3) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
((((triple3) -> (rule4 % int4)) ((((((triple3) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4