Anne is cold. Dave is red. Erin is blue. If something is cold and round then it is smart. All blue things are red. Cold things are round. If something is smart and quiet then it is round. All red things are kind. If something is red then it is cold.
Anne is cold.
("Anne" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Erin is blue.
("Erin" "is" "blue" "+")
If something is cold and round then it is smart.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
All blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Cold things are round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is smart and quiet then it is round.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
All red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something is red then it is cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
Erin is blue.
True
1
proof
[(triple3)]
("Erin" "is" "blue" "+")
triple3
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Dave is cold.
True
2
proof
[(((triple2) -> rule6))]
("Dave" "is" "cold" "+")
((triple2) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not kind.
False
2
inv-proof
[(((triple2) -> rule5))]
("Dave" "is" "kind" "-")
((triple2) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Erin is kind.
True
3
proof
[(((((triple3) -> rule2)) -> rule5))]
("Erin" "is" "kind" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not cold.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule6))]
("Erin" "is" "cold" "-")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Dave is smart.
True
6
proof
[(((((triple2) -> rule6) ((((triple2) -> rule6)) -> rule3)) -> rule1))]
("Dave" "is" "smart" "+")
((((triple2) -> (rule6 % int3)) ((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is not smart.
False
6
inv-proof
[(((((triple2) -> rule6) ((((triple2) -> rule6)) -> rule3)) -> rule1))]
("Dave" "is" "smart" "-")
((((triple2) -> (rule6 % int3)) ((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Anne is not kind.
Unknown
inv-rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is red.
Unknown
rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "red" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Anne is cold.[(triple1)] Dave is red.[(triple2)] Erin is blue.[(triple3)] @1: Anne is round.[(((triple1) -> rule3))] Dave is cold.[(((triple2) -> rule6))] Dave is kind.[(((triple2) -> rule5))] Erin is red.[(((triple3) -> rule2))] @2: Anne is smart.[(((triple1 ((triple1) -> rule3)) -> rule1))] Dave is round.[(((((triple2) -> rule6)) -> rule3))] Erin is cold.[(((((triple3) -> rule2)) -> rule6))] Erin is kind.[(((((triple3) -> rule2)) -> rule5))] @3: Dave is smart.[(((((triple2) -> rule6) ((((triple2) -> rule6)) -> rule3)) -> rule1))] Erin is round.[(((((((triple3) -> rule2)) -> rule6)) -> rule3))] @4: Erin is smart.[(((((((triple3) -> rule2)) -> rule6) ((((((triple3) -> rule2)) -> rule6)) -> rule3)) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple2) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple2) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple3) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple2) -> (rule6 % int3)) ((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
((((((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
((((((triple3) -> (rule2 % int4))) -> (rule6 % int3)) ((((((triple3) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4