Anne is cold. Bob is nice. Dave is nice. Gary is rough. If someone is rough and nice then they are cold. All cold, rough people are round. If someone is nice then they are round. If Gary is green then Gary is quiet. If someone is white then they are quiet. If someone is cold then they are green. If someone is round then they are cold. If Bob is nice then Bob is round.
Anne is cold.
("Anne" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If someone is rough and nice then they are cold.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
All cold, rough people are round.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If someone is nice then they are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If Gary is green then Gary is quiet.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "quiet" "+"))
If someone is white then they are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If someone is cold then they are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is round then they are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If Bob is nice then Bob is round.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "round" "+"))
Gary is rough.
True
1
proof
[(triple4)]
("Gary" "is" "rough" "+")
triple4
Bob is not nice.
False
1
inv-proof
[(triple2)]
("Bob" "is" "nice" "-")
triple2
Anne is green.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "green" "+")
((triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple2) -> rule3) OR ((triple2) -> rule8))]
("Bob" "is" "round" "-")
((triple2) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple2) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is cold.
True
3
proof
[(((((triple3) -> rule3)) -> rule7))]
("Dave" "is" "cold" "+")
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Bob is not cold.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule7) OR ((((triple2) -> rule8)) -> rule7))]
("Bob" "is" "cold" "-")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple2) -> (rule8 % int2))) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
True
4
proof
[(((((((triple2) -> rule3)) -> rule7)) -> rule6) OR ((((((triple2) -> rule8)) -> rule7)) -> rule6))]
("Bob" "is" "green" "+")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((((triple2) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not green.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule7)) -> rule6) OR ((((((triple2) -> rule8)) -> rule7)) -> rule6))]
("Bob" "is" "green" "-")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((((triple2) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "quiet" "-")
Gary is cold.
Unknown
rconc
[@3: Gary is cold.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule1 <- FAIL)]]
("Gary" "is" "cold" "+")
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "round" "-")
Gary is green.
Unknown
rconc
[@4: Gary is green.[CWA. Example of deepest failure = (rule6 <- rule7 <- rule2 <- rule1 <- FAIL)]]
("Gary" "is" "green" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Anne is cold.[(triple1)] Bob is nice.[(triple2)] Dave is nice.[(triple3)] Gary is rough.[(triple4)] @1: Anne is green.[(((triple1) -> rule6))] Bob is round.[(((triple2) -> rule3) OR ((triple2) -> rule8))] Dave is round.[(((triple3) -> rule3))] @2: Bob is cold.[(((((triple2) -> rule3)) -> rule7) OR ((((triple2) -> rule8)) -> rule7))] Dave is cold.[(((((triple3) -> rule3)) -> rule7))] @3: Bob is green.[(((((((triple2) -> rule3)) -> rule7)) -> rule6) OR ((((((triple2) -> rule8)) -> rule7)) -> rule6))] Dave is green.[(((((((triple3) -> rule3)) -> rule7)) -> rule6))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Gary is rough.
("Gary" "is" "rough" "+")
triple4
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple2) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple2) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple3) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple2) -> (rule8 % int2))) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((((triple2) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
((((((triple3) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3