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