Anne is green. Bob is furry. Dave is cold. All furry, green things are round. Cold, quiet things are not round. All furry things are round. All furry, round things are green. If something is quiet and round then it is green. Round things are blue. Blue things are quiet. If something is green then it is red.
Anne is green.
("Anne" "is" "green" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Dave is cold.
("Dave" "is" "cold" "+")
All furry, green things are round.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Cold, quiet things are not round.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "-"))
All furry things are round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
All furry, round things are green.
((("something" "is" "furry" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something is quiet and round then it is green.
((("something" "is" "quiet" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If something is green then it is red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Dave is cold.
True
1
proof
[(triple3)]
("Dave" "is" "cold" "+")
triple3
Bob is not furry.
False
1
inv-proof
[(triple2)]
("Bob" "is" "furry" "-")
triple2
Anne is red.
True
2
proof
[(((triple1) -> rule8))]
("Anne" "is" "red" "+")
((triple1) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple2) -> rule3))]
("Bob" "is" "round" "-")
((triple2) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
True
4
proof
[(((triple2 ((triple2) -> rule3)) -> rule4) OR ((((((((triple2) -> rule3)) -> rule6)) -> rule7) ((triple2) -> rule3)) -> rule5))]
("Bob" "is" "green" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((((((triple2) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule7 % int2)) ((triple2) -> (rule3 % int4))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is not green.
False
4
inv-proof
[(((triple2 ((triple2) -> rule3)) -> rule4) OR ((((((((triple2) -> rule3)) -> rule6)) -> rule7) ((triple2) -> rule3)) -> rule5))]
("Bob" "is" "green" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((((((triple2) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule7 % int2)) ((triple2) -> (rule3 % int4))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is red.
True
5
proof
[(((((triple2 ((triple2) -> rule3)) -> rule4)) -> rule8) OR ((((((((((triple2) -> rule3)) -> rule6)) -> rule7) ((triple2) -> rule3)) -> rule5)) -> rule8))]
("Bob" "is" "red" "+")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((((((((triple2) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule7 % int3)) ((triple2) -> (rule3 % int5))) -> (rule5 % int2))) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
int5
Bob is not quiet.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule6)) -> rule7))]
("Bob" "is" "quiet" "-")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Dave is not blue.
Unknown
inv-rconc
[@2: Dave is blue.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is green.
Unknown
rconc
[@2: Dave is green.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Dave" "is" "green" "+")
Anne is not blue.
Unknown
inv-rconc
[@2: Anne is blue.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Anne" "is" "blue" "-")
Dave is red.
Unknown
rconc
[@3: Dave is red.[CWA. Example of deepest failure = (rule8 <- rule5 <- rule1 <- FAIL)]]
("Dave" "is" "red" "+")
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" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is green.[(triple1)] Bob is furry.[(triple2)] Dave is cold.[(triple3)] @1: Anne is red.[(((triple1) -> rule8))] Bob is round.[(((triple2) -> rule3))] @2: Bob is blue.[(((((triple2) -> rule3)) -> rule6))] Bob is green.[(((triple2 ((triple2) -> rule3)) -> rule4) OR ((((((((triple2) -> rule3)) -> rule6)) -> rule7) ((triple2) -> rule3)) -> rule5))] @3: Bob is quiet.[(((((((triple2) -> rule3)) -> rule6)) -> rule7))] Bob is red.[(((((triple2 ((triple2) -> rule3)) -> rule4)) -> rule8) OR ((((((((((triple2) -> rule3)) -> rule6)) -> rule7) ((triple2) -> rule3)) -> rule5)) -> rule8))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple2) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((((((triple2) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule7 % int2)) ((triple2) -> (rule3 % int4))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((((((((triple2) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule7 % int3)) ((triple2) -> (rule3 % int5))) -> (rule5 % int2))) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
int5