Charlie is cold. Dave is red. Gary is cold. If something is furry then it is blue. If something is cold then it is green. Green things are furry.
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If something is furry then it is blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
If something is cold then it is green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
Green things are furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
Charlie is cold.
True
1
proof
[(triple1)]
("Charlie" "is" "cold" "+")
triple1
Charlie is not cold.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "cold" "-")
triple1
Charlie is green.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "green" "+")
((triple1) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple3) -> rule2))]
("Gary" "is" "green" "-")
((triple3) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Gary" "is" "furry" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not furry.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("Gary" "is" "furry" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is blue.
True
4
proof
[(((((((triple3) -> rule2)) -> rule3)) -> rule1))]
("Gary" "is" "blue" "+")
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Charlie is not blue.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule1))]
("Charlie" "is" "blue" "-")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Dave is not furry.
Unknown
inv-rconc
[@2: Dave is furry.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not blue.
Unknown
inv-rconc
[@3: Dave is blue.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule2 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Charlie is cold.[(triple1)] Dave is red.[(triple2)] Gary is cold.[(triple3)] @1: Charlie is green.[(((triple1) -> rule2))] Gary is green.[(((triple3) -> rule2))] @2: Charlie is furry.[(((((triple1) -> rule2)) -> rule3))] Gary is furry.[(((((triple3) -> rule2)) -> rule3))] @3: Charlie is blue.[(((((((triple1) -> rule2)) -> rule3)) -> rule1))] Gary is blue.[(((((((triple3) -> rule2)) -> rule3)) -> rule1))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple3) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3