Anne is blue. Erin is big. Erin is nice. Erin is smart. Gary is nice. Gary is quiet. Harry is smart. Round things are not big. If something is furry then it is big. If Harry is not nice then Harry is not big. All nice things are smart. If something is nice and round then it is smart. If something is smart then it is blue. All blue, nice things are not round. If something is furry and not blue then it is quiet.
Anne is blue.
("Anne" "is" "blue" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Round things are not big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "-"))
If something is furry then it is big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If Harry is not nice then Harry is not big.
((("Harry" "is" "nice" "~")) -> ("Harry" "is" "big" "-"))
All nice things are smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If something is nice and round then it is smart.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If something is smart then it is blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
All blue, nice things are not round.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "-"))
If something is furry and not blue then it is quiet.
((("something" "is" "furry" "+") ("something" "is" "blue" "~")) -> ("something" "is" "quiet" "+"))
Erin is nice.
True
1
proof
[(triple3)]
("Erin" "is" "nice" "+")
triple3
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Harry is blue.
True
2
proof
[(((triple7) -> rule6))]
("Harry" "is" "blue" "+")
((triple7) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple7) -> rule6))]
("Harry" "is" "blue" "-")
((triple7) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Gary is blue.
True
3
proof
[(((((triple5) -> rule4)) -> rule6))]
("Gary" "is" "blue" "+")
((((triple5) -> (rule4 % int2))) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not blue.
False
3
inv-proof
[(((((triple5) -> rule4)) -> rule6))]
("Gary" "is" "blue" "-")
((((triple5) -> (rule4 % int2))) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not round.
True
5
proof
[(((((((triple5) -> rule4)) -> rule6) triple5) -> rule7))]
("Gary" "is" "round" "-")
((((((triple5) -> (rule4 % int3))) -> (rule6 % int2)) triple5) -> (rule7 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is round.
False
5
inv-proof
[(((((((triple5) -> rule4)) -> rule6) triple5) -> rule7))]
("Gary" "is" "round" "+")
((((((triple5) -> (rule4 % int3))) -> (rule6 % int2)) triple5) -> (rule7 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "big" "-")
Anne is smart.
Unknown
rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "smart" "+")
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "big" "-")
Harry is quiet.
Unknown
rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "quiet" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is blue.[(triple1)] Erin is big.[(triple2)] Erin is nice.[(triple3)] Erin is smart.[(triple4 OR ((triple3) -> rule4))] Gary is nice.[(triple5)] Gary is quiet.[(triple6)] Harry is smart.[(triple7)] @1: Erin is blue.[(((triple4) -> rule6) OR ((((triple3) -> rule4)) -> rule6))] Gary is smart.[(((triple5) -> rule4))] Harry is blue.[(((triple7) -> rule6))] @2: Erin is not round.[(((((triple4) -> rule6) triple3) -> rule7) OR ((((((triple3) -> rule4)) -> rule6) triple3) -> rule7))] Gary is blue.[(((((triple5) -> rule4)) -> rule6))] @3: Gary is not round.[(((((((triple5) -> rule4)) -> rule6) triple5) -> rule7))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
triple4
((triple3) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Erin is blue.
("Erin" "is" "blue" "+")
((triple4) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((triple5) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple7) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Erin is not round.
("Erin" "is" "round" "-")
((((triple4) -> (rule6 % int2)) triple3) -> (rule7 % int1))
Erin is not round.
("Erin" "is" "round" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2)) triple3) -> (rule7 % int1))
Erin is not round.
("Erin" "is" "round" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
((((triple5) -> (rule4 % int2))) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not round.
("Gary" "is" "round" "-")
((((((triple5) -> (rule4 % int3))) -> (rule6 % int2)) triple5) -> (rule7 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3