Anne is cold. Anne is white. Bob is rough. Bob is round. Bob is not white. Charlie is not blue. Dave is blue. If someone is cold and round then they are rough. All cold, kind people are blue. All green people are round. Cold people are green. Rough people are kind.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is not white.
("Bob" "is" "white" "-")
Charlie is not blue.
("Charlie" "is" "blue" "-")
Dave is blue.
("Dave" "is" "blue" "+")
If someone is cold and round then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All cold, kind people are blue.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
All green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Cold people are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
Rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Anne is cold.
True
1
proof
[(triple1)]
("Anne" "is" "cold" "+")
triple1
Bob is not round.
False
1
inv-proof
[(triple4)]
("Bob" "is" "round" "-")
triple4
Anne is green.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "green" "+")
((triple1) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple3) -> rule5))]
("Bob" "is" "kind" "-")
((triple3) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Anne is round.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("Anne" "is" "round" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not round.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("Anne" "is" "round" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is rough.
True
5
proof
[(((triple1 ((((triple1) -> rule4)) -> rule3)) -> rule1))]
("Anne" "is" "rough" "+")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not rough.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule4)) -> rule3)) -> rule1))]
("Anne" "is" "rough" "-")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is kind.
True
6
proof
[(((((triple1 ((((triple1) -> rule4)) -> rule3)) -> rule1)) -> rule5))]
("Anne" "is" "kind" "+")
((((triple1 ((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is not kind.
False
6
inv-proof
[(((((triple1 ((((triple1) -> rule4)) -> rule3)) -> rule1)) -> rule5))]
("Anne" "is" "kind" "-")
((((triple1 ((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is blue.
True
8
proof
[(((triple1 ((((triple1 ((((triple1) -> rule4)) -> rule3)) -> rule1)) -> rule5)) -> rule2))]
("Anne" "is" "blue" "+")
((triple1 ((((triple1 ((((triple1) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
Anne is not blue.
False
8
inv-proof
[(((triple1 ((((triple1 ((((triple1) -> rule4)) -> rule3)) -> rule1)) -> rule5)) -> rule2))]
("Anne" "is" "blue" "-")
((triple1 ((((triple1 ((((triple1) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "rough" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not round.
Unknown
inv-rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Charlie" "is" "round" "-")
Dave is round.
Unknown
rconc
[@2: Dave is round.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Dave" "is" "round" "+")
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "rough" "-")
Dave is kind.
Unknown
rconc
[@2: Dave is kind.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Dave" "is" "kind" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Anne is cold.[(triple1)] Anne is white.[(triple2)] Bob is not white.[(triple5)] Bob is rough.[(triple3)] Bob is round.[(triple4)] Charlie is not blue.[(triple6)] Dave is blue.[(triple7)] @1: Anne is green.[(((triple1) -> rule4))] Bob is kind.[(((triple3) -> rule5))] @2: Anne is round.[(((((triple1) -> rule4)) -> rule3))] @3: Anne is rough.[(((triple1 ((((triple1) -> rule4)) -> rule3)) -> rule1))] @4: Anne is kind.[(((((triple1 ((((triple1) -> rule4)) -> rule3)) -> rule1)) -> rule5))] @5: Anne is blue.[(((triple1 ((((triple1 ((((triple1) -> rule4)) -> rule3)) -> rule1)) -> rule5)) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Bob is not white.
("Bob" "is" "white" "-")
triple5
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple6
Dave is blue.
("Dave" "is" "blue" "+")
triple7
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple3) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1 ((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is blue.
("Anne" "is" "blue" "+")
((triple1 ((((triple1 ((((triple1) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
int5