Anne is smart. Dave is young. Gary is not cold. Gary is not rough. Harry is round. Harry is smart. Harry is young. If someone is smart then they are nice. If Harry is rough then Harry is round. If someone is nice and not young then they are round. All smart, nice people are round. If someone is cold and nice then they are not smart. If someone is young and not rough then they are smart. If someone is round and not nice then they are quiet. Round people are quiet.
Anne is smart.
("Anne" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is not rough.
("Gary" "is" "rough" "-")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is smart then they are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If Harry is rough then Harry is round.
((("Harry" "is" "rough" "+")) -> ("Harry" "is" "round" "+"))
If someone is nice and not young then they are round.
((("someone" "is" "nice" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "round" "+"))
All smart, nice people are round.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If someone is cold and nice then they are not smart.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "-"))
If someone is young and not rough then they are smart.
((("someone" "is" "young" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "smart" "+"))
If someone is round and not nice then they are quiet.
((("someone" "is" "round" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "quiet" "+"))
Round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
Harry is round.
True
1
proof
[(triple5 OR ((triple6 ((triple6) -> rule1)) -> rule4))]
("Harry" "is" "round" "+")
triple5
((triple6 ((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not young.
False
1
inv-proof
[(triple7)]
("Harry" "is" "young" "-")
triple7
Harry is quiet.
True
2
proof
[(((triple5) -> rule8) OR ((((triple6 ((triple6) -> rule1)) -> rule4)) -> rule8))]
("Harry" "is" "quiet" "+")
((triple5) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple6 ((triple6) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Anne is not nice.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "nice" "-")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule4))]
("Anne" "is" "round" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not round.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule4))]
("Anne" "is" "round" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is quiet.
True
5
proof
[(((((triple1 ((triple1) -> rule1)) -> rule4)) -> rule8))]
("Anne" "is" "quiet" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is not quiet.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule1)) -> rule4)) -> rule8))]
("Anne" "is" "quiet" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is nice.
Unknown
rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Dave" "is" "nice" "+")
Dave is not round.
Unknown
inv-rconc
[@2: Dave is round.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Dave" "is" "round" "-")
Gary is nice.
Unknown
rconc
[@2: Gary is nice.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Gary" "is" "nice" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Anne is smart.[(triple1)] Dave is young.[(triple2)] Gary is not cold.[(triple3)] Gary is not rough.[(triple4)] Harry is round.[(triple5 OR ((triple6 ((triple6) -> rule1)) -> rule4))] Harry is smart.[(triple6)] Harry is young.[(triple7)] @1: Anne is nice.[(((triple1) -> rule1))] Harry is nice.[(((triple6) -> rule1))] Harry is quiet.[(((triple5) -> rule8) OR ((((triple6 ((triple6) -> rule1)) -> rule4)) -> rule8))] @2: Anne is round.[(((triple1 ((triple1) -> rule1)) -> rule4))] @3: Anne is quiet.[(((((triple1 ((triple1) -> rule1)) -> rule4)) -> rule8))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple2
Gary is not cold.
("Gary" "is" "cold" "-")
triple3
Gary is not rough.
("Gary" "is" "rough" "-")
triple4
Harry is round.
("Harry" "is" "round" "+")
triple5
((triple6 ((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple6) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple5) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple6 ((triple6) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3