Anne is cold. Bob is cold. Bob is green. Bob is quiet. Charlie is not cold. Charlie is furry. Charlie is not green. Charlie is quiet. Erin is furry. Erin is smart. If something is furry and rough then it is green. Round things are quiet. If something is quiet and smart then it is not cold. If something is rough then it is furry. Smart, furry things are round. If Anne is smart and Anne is green then Anne is rough.
Anne is cold.
("Anne" "is" "cold" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If something is furry and rough then it is green.
((("something" "is" "furry" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
Round things are quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet and smart then it is not cold.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "-"))
If something is rough then it is furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
Smart, furry things are round.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If Anne is smart and Anne is green then Anne is rough.
((("Anne" "is" "smart" "+") ("Anne" "is" "green" "+")) -> ("Anne" "is" "rough" "+"))
Bob is cold.
True
1
proof
[(triple2)]
("Bob" "is" "cold" "+")
triple2
Erin is not smart.
False
1
inv-proof
[(triple10)]
("Erin" "is" "smart" "-")
triple10
Erin is round.
True
3
proof
[(((triple10 triple9) -> rule5))]
("Erin" "is" "round" "+")
((triple10 triple9) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not round.
False
3
inv-proof
[(((triple10 triple9) -> rule5))]
("Erin" "is" "round" "-")
((triple10 triple9) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
True
4
proof
[(((((triple10 triple9) -> rule5)) -> rule2))]
("Erin" "is" "quiet" "+")
((((triple10 triple9) -> (rule5 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not quiet.
False
4
inv-proof
[(((((triple10 triple9) -> rule5)) -> rule2))]
("Erin" "is" "quiet" "-")
((((triple10 triple9) -> (rule5 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not cold.
True
6
proof
[(((((((triple10 triple9) -> rule5)) -> rule2) triple10) -> rule3))]
("Erin" "is" "cold" "-")
((((((triple10 triple9) -> (rule5 % int3))) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is cold.
False
6
inv-proof
[(((((((triple10 triple9) -> rule5)) -> rule2) triple10) -> rule3))]
("Erin" "is" "cold" "+")
((((((triple10 triple9) -> (rule5 % int3))) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Anne is not quiet.
Unknown
inv-rconc
[@2: Anne is quiet.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is round.
Unknown
rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "round" "+")
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is furry.
Unknown
rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "furry" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Anne is cold.[(triple1)] Bob is cold.[(triple2)] Bob is green.[(triple3)] Bob is quiet.[(triple4)] Charlie is furry.[(triple6)] Charlie is not cold.[(triple5)] Charlie is not green.[(triple7)] Charlie is quiet.[(triple8)] Erin is furry.[(triple9)] Erin is smart.[(triple10)] @1: Erin is round.[(((triple10 triple9) -> rule5))] @2: Erin is quiet.[(((((triple10 triple9) -> rule5)) -> rule2))] @3: Erin is not cold.[(((((((triple10 triple9) -> rule5)) -> rule2) triple10) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple5
Charlie is not green.
("Charlie" "is" "green" "-")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple8
Erin is furry.
("Erin" "is" "furry" "+")
triple9
Erin is smart.
("Erin" "is" "smart" "+")
triple10
Erin is round.
("Erin" "is" "round" "+")
((triple10 triple9) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple10 triple9) -> (rule5 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not cold.
("Erin" "is" "cold" "-")
((((((triple10 triple9) -> (rule5 % int3))) -> (rule2 % int2)) triple10) -> (rule3 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3