Anne is nice. Anne is smart. Erin is cold. Erin is green. Erin is kind. Erin is nice. Fiona is nice. Harry is cold. Harry is kind. Harry is quiet. Harry is red. Harry is smart. If something is smart and green then it is quiet. All nice, red things are green. All green things are smart.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is smart and green then it is quiet.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
All nice, red things are green.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
All green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Erin is kind.
True
1
proof
[(triple5)]
("Erin" "is" "kind" "+")
triple5
Harry is not red.
False
1
inv-proof
[(triple11)]
("Harry" "is" "red" "-")
triple11
Erin is smart.
True
2
proof
[(((triple4) -> rule3))]
("Erin" "is" "smart" "+")
((triple4) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple4) -> rule3))]
("Erin" "is" "smart" "-")
((triple4) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is quiet.
True
4
proof
[(((((triple4) -> rule3) triple4) -> rule1))]
("Erin" "is" "quiet" "+")
((((triple4) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not quiet.
False
4
inv-proof
[(((((triple4) -> rule3) triple4) -> rule1))]
("Erin" "is" "quiet" "-")
((((triple4) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "green" "-")
Anne is green.
Unknown
rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "green" "+")
Fiona is not smart.
Unknown
inv-rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Anne is nice.[(triple1)] Anne is smart.[(triple2)] Erin is cold.[(triple3)] Erin is green.[(triple4)] Erin is kind.[(triple5)] Erin is nice.[(triple6)] Fiona is nice.[(triple7)] Harry is cold.[(triple8)] Harry is kind.[(triple9)] Harry is quiet.[(triple10)] Harry is red.[(triple11)] Harry is smart.[(triple12)] @1: Erin is smart.[(((triple4) -> rule3))] @2: Erin is quiet.[(((((triple4) -> rule3) triple4) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Erin is nice.
("Erin" "is" "nice" "+")
triple6
Fiona is nice.
("Fiona" "is" "nice" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Erin is smart.
("Erin" "is" "smart" "+")
((triple4) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple4) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2