Anne is rough. Anne is smart. Erin is cold. Erin is quiet. Erin is not smart. Harry is cold. Harry is not smart. Cold, white people are quiet. All smart people are cold. If someone is cold then they are round.
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
Cold, white people are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
All smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold then they are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
Erin is quiet.
True
1
proof
[(triple4)]
("Erin" "is" "quiet" "+")
triple4
Erin is smart.
False
1
inv-proof
[(triple5)]
("Erin" "is" "smart" "+")
triple5
Anne is cold.
True
2
proof
[(((triple2) -> rule2))]
("Anne" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple6) -> rule3))]
("Harry" "is" "round" "-")
((triple6) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Anne is round.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("Anne" "is" "round" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not round.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("Anne" "is" "round" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "quiet" "-")
Harry is quiet.
Unknown
rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "quiet" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Anne is rough.[(triple1)] Anne is smart.[(triple2)] Erin is cold.[(triple3)] Erin is not smart.[(triple5)] Erin is quiet.[(triple4)] Harry is cold.[(triple6)] Harry is not smart.[(triple7)] @1: Anne is cold.[(((triple2) -> rule2))] Erin is round.[(((triple3) -> rule3))] Harry is round.[(((triple6) -> rule3))] @2: Anne is round.[(((((triple2) -> rule2)) -> rule3))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Erin is not smart.
("Erin" "is" "smart" "-")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is not smart.
("Harry" "is" "smart" "-")
triple7
Anne is cold.
("Anne" "is" "cold" "+")
((triple2) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple3) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple6) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2