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