Anne is cold. Anne is nice. Anne is young. Erin is furry. Gary is furry. Gary is quiet. Gary is not rough. Gary is smart. Harry is furry. Harry is nice. Harry is smart. Harry is not young. If something is quiet then it is nice. If something is smart and not young then it is rough. All furry things are quiet. If Harry is quiet then Harry is smart. Nice things are smart. If Anne is smart and Anne is not cold then Anne is rough. If Gary is cold and Gary is nice then Gary is smart. If Gary is smart then Gary is cold.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is young.
("Anne" "is" "young" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is not young.
("Harry" "is" "young" "-")
If something is quiet then it is nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
If something is smart and not young then it is rough.
((("something" "is" "smart" "+") ("something" "is" "young" "~")) -> ("something" "is" "rough" "+"))
All furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If Harry is quiet then Harry is smart.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "smart" "+"))
Nice things are smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If Anne is smart and Anne is not cold then Anne is rough.
((("Anne" "is" "smart" "+") ("Anne" "is" "cold" "~")) -> ("Anne" "is" "rough" "+"))
If Gary is cold and Gary is nice then Gary is smart.
((("Gary" "is" "cold" "+") ("Gary" "is" "nice" "+")) -> ("Gary" "is" "smart" "+"))
If Gary is smart then Gary is cold.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "cold" "+"))
Harry is not young.
True
1
proof
[(triple12)]
("Harry" "is" "young" "-")
triple12
Anne is not young.
False
1
inv-proof
[(triple3)]
("Anne" "is" "young" "-")
triple3
Anne is smart.
True
2
proof
[(((triple2) -> rule5))]
("Anne" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple9) -> rule3))]
("Harry" "is" "quiet" "-")
((triple9) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Erin is nice.
True
3
proof
[(((((triple4) -> rule3)) -> rule1))]
("Erin" "is" "nice" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is not nice.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule1))]
("Erin" "is" "nice" "-")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "quiet" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "rough" "+")
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "rough" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Anne is cold.[(triple1)] Anne is nice.[(triple2)] Anne is young.[(triple3)] Erin is furry.[(triple4)] Gary is furry.[(triple5)] Gary is not rough.[(triple7)] Gary is quiet.[(triple6 OR ((triple5) -> rule3))] Gary is smart.[(triple8 OR ((((triple6) -> rule1)) -> rule5) OR ((((((triple5) -> rule3)) -> rule1)) -> rule5))] Harry is furry.[(triple9)] Harry is nice.[(triple10 OR ((((triple9) -> rule3)) -> rule1))] Harry is not young.[(triple12)] Harry is smart.[(triple11 OR ((triple10) -> rule5) OR ((((triple9) -> rule3)) -> rule4) OR ((((((triple9) -> rule3)) -> rule1)) -> rule5))] @1: Anne is smart.[(((triple2) -> rule5))] Erin is quiet.[(((triple4) -> rule3))] Gary is cold.[(((triple8) -> rule8) OR ((((((triple6) -> rule1)) -> rule5)) -> rule8) OR ((((((((triple5) -> rule3)) -> rule1)) -> rule5)) -> rule8))] Gary is nice.[(((triple6) -> rule1) OR ((((triple5) -> rule3)) -> rule1))] Harry is quiet.[(((triple9) -> rule3))] Harry is rough.[(((triple11 triple12) -> rule2) OR ((((triple10) -> rule5) triple12) -> rule2) OR ((((((triple9) -> rule3)) -> rule4) triple12) -> rule2) OR ((((((((triple9) -> rule3)) -> rule1)) -> rule5) triple12) -> rule2))] @2: Erin is nice.[(((((triple4) -> rule3)) -> rule1))] @3: Erin is smart.[(((((((triple4) -> rule3)) -> rule1)) -> rule5))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
triple4
Gary is furry.
("Gary" "is" "furry" "+")
triple5
Gary is not rough.
("Gary" "is" "rough" "-")
triple7
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
((triple5) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple8
((((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not young.
("Harry" "is" "young" "-")
triple12
Harry is smart.
("Harry" "is" "smart" "+")
triple11
((triple10) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((((triple9) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple4) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple8) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((((triple6) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((((triple5) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is nice.
("Gary" "is" "nice" "+")
((triple6) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple9) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple11 triple12) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple10) -> (rule5 % int2)) triple12) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((((triple9) -> (rule3 % int3))) -> (rule4 % int2)) triple12) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((((triple9) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) triple12) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Erin is nice.
("Erin" "is" "nice" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3