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