Anne is cold. Anne is red. Anne is smart. Bob is cold. Charlie is not red. Dave is not cold. Dave is smart. All nice things are quiet. Smart things are white. If something is red then it is not round. If something is white and not cold then it is nice. All nice, quiet things are red. White, red things are smart.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is smart.
("Dave" "is" "smart" "+")
All nice things are quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
Smart things are white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is red then it is not round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "-"))
If something is white and not cold then it is nice.
((("something" "is" "white" "+") ("something" "is" "cold" "~")) -> ("something" "is" "nice" "+"))
All nice, quiet things are red.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
White, red things are smart.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
Anne is smart.
True
1
proof
[(triple3)]
("Anne" "is" "smart" "+")
triple3
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Anne is white.
True
2
proof
[(((triple3) -> rule2))]
("Anne" "is" "white" "+")
((triple3) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not white.
False
2
inv-proof
[(((triple3) -> rule2))]
("Anne" "is" "white" "-")
((triple3) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Dave is nice.
True
4
proof
[(((((triple7) -> rule2) triple6) -> rule4))]
("Dave" "is" "nice" "+")
((((triple7) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not nice.
False
4
inv-proof
[(((((triple7) -> rule2) triple6) -> rule4))]
("Dave" "is" "nice" "-")
((((triple7) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is quiet.
True
5
proof
[(((((((triple7) -> rule2) triple6) -> rule4)) -> rule1))]
("Dave" "is" "quiet" "+")
((((((triple7) -> (rule2 % int3)) triple6) -> (rule4 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not quiet.
False
5
inv-proof
[(((((((triple7) -> rule2) triple6) -> rule4)) -> rule1))]
("Dave" "is" "quiet" "-")
((((((triple7) -> (rule2 % int3)) triple6) -> (rule4 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is red.
True
10
proof
[(((((((triple7) -> rule2) triple6) -> rule4) ((((((triple7) -> rule2) triple6) -> rule4)) -> rule1)) -> rule5))]
("Dave" "is" "red" "+")
((((((triple7) -> (rule2 % int4)) triple6) -> (rule4 % int3)) ((((((triple7) -> (rule2 % int4)) triple6) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is not red.
False
10
inv-proof
[(((((((triple7) -> rule2) triple6) -> rule4) ((((((triple7) -> rule2) triple6) -> rule4)) -> rule1)) -> rule5))]
("Dave" "is" "red" "-")
((((((triple7) -> (rule2 % int4)) triple6) -> (rule4 % int3)) ((((((triple7) -> (rule2 % int4)) triple6) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is not round.
True
11
proof
[(((((((((triple7) -> rule2) triple6) -> rule4) ((((((triple7) -> rule2) triple6) -> rule4)) -> rule1)) -> rule5)) -> rule3))]
("Dave" "is" "round" "-")
((((((((triple7) -> (rule2 % int5)) triple6) -> (rule4 % int4)) ((((((triple7) -> (rule2 % int5)) triple6) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
int5
Dave is round.
False
11
inv-proof
[(((((((((triple7) -> rule2) triple6) -> rule4) ((((((triple7) -> rule2) triple6) -> rule4)) -> rule1)) -> rule5)) -> rule3))]
("Dave" "is" "round" "+")
((((((((triple7) -> (rule2 % int5)) triple6) -> (rule4 % int4)) ((((((triple7) -> (rule2 % int5)) triple6) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
int5
Charlie is not white.
Unknown
inv-rconc
[@2: Charlie is white.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Charlie" "is" "white" "-")
Bob is quiet.
Unknown
rconc
[@2: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not smart.
Unknown
inv-rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Bob" "is" "smart" "-")
Charlie is quiet.
Unknown
rconc
[@2: Charlie is quiet.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Anne is not quiet.
Unknown
inv-rconc
[@2: Anne is quiet.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Anne" "is" "quiet" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Anne is cold.[(triple1)] Anne is red.[(triple2)] Anne is smart.[(triple3)] Bob is cold.[(triple4)] Charlie is not red.[(triple5)] Dave is not cold.[(triple6)] Dave is smart.[(triple7)] @1: Anne is not round.[(((triple2) -> rule3))] Anne is white.[(((triple3) -> rule2))] Dave is white.[(((triple7) -> rule2))] @2: Dave is nice.[(((((triple7) -> rule2) triple6) -> rule4))] @3: Dave is quiet.[(((((((triple7) -> rule2) triple6) -> rule4)) -> rule1))] @4: Dave is red.[(((((((triple7) -> rule2) triple6) -> rule4) ((((((triple7) -> rule2) triple6) -> rule4)) -> rule1)) -> rule5))] @5: Dave is not round.[(((((((((triple7) -> rule2) triple6) -> rule4) ((((((triple7) -> rule2) triple6) -> rule4)) -> rule1)) -> rule5)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
triple4
Charlie is not red.
("Charlie" "is" "red" "-")
triple5
Dave is not cold.
("Dave" "is" "cold" "-")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Anne is not round.
("Anne" "is" "round" "-")
((triple2) -> (rule3 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
((triple3) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple7) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple7) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((((triple7) -> (rule2 % int3)) triple6) -> (rule4 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((((((triple7) -> (rule2 % int4)) triple6) -> (rule4 % int3)) ((((((triple7) -> (rule2 % int4)) triple6) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is not round.
("Dave" "is" "round" "-")
((((((((triple7) -> (rule2 % int5)) triple6) -> (rule4 % int4)) ((((((triple7) -> (rule2 % int5)) triple6) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
int5