Gary is nice. Harry is not nice. If Gary is round then Gary is smart. If Harry is round and Harry is young then Harry is nice. All nice people are round. If someone is round then they are quiet. If someone is smart and nice then they are blue. If someone is blue and not quiet then they are not cold. All blue, young people are cold. Quiet, cold people are smart.
Gary is nice.
("Gary" "is" "nice" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
If Gary is round then Gary is smart.
((("Gary" "is" "round" "+")) -> ("Gary" "is" "smart" "+"))
If Harry is round and Harry is young then Harry is nice.
((("Harry" "is" "round" "+") ("Harry" "is" "young" "+")) -> ("Harry" "is" "nice" "+"))
All nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If someone is smart and nice then they are blue.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue and not quiet then they are not cold.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "cold" "-"))
All blue, young people are cold.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
Quiet, cold people are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Gary is nice.
True
1
proof
[(triple1)]
("Gary" "is" "nice" "+")
triple1
Harry is nice.
False
1
inv-proof
[(triple2)]
("Harry" "is" "nice" "+")
triple2
Gary is round.
True
2
proof
[(((triple1) -> rule3))]
("Gary" "is" "round" "+")
((triple1) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is not round.
False
2
inv-proof
[(((triple1) -> rule3))]
("Gary" "is" "round" "-")
((triple1) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Gary" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not quiet.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule4))]
("Gary" "is" "quiet" "-")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is blue.
True
5
proof
[(((((((triple1) -> rule3)) -> rule1) triple1) -> rule5))]
("Gary" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is not blue.
False
5
inv-proof
[(((((((triple1) -> rule3)) -> rule1) triple1) -> rule5))]
("Gary" "is" "blue" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Harry is not quiet.
Unknown
inv-rconc
[@2: Harry is quiet.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Harry" "is" "quiet" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "cold" "+")
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "blue" "-")
Harry is cold.
Unknown
rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "cold" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Gary is nice.[(triple1)] Harry is not nice.[(triple2)] @1: Gary is round.[(((triple1) -> rule3))] @2: Gary is quiet.[(((((triple1) -> rule3)) -> rule4))] Gary is smart.[(((((triple1) -> rule3)) -> rule1))] @3: Gary is blue.[(((((((triple1) -> rule3)) -> rule1) triple1) -> rule5))]
Gary is nice.
("Gary" "is" "nice" "+")
triple1
Harry is not nice.
("Harry" "is" "nice" "-")
triple2
Gary is round.
("Gary" "is" "round" "+")
((triple1) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3