Charlie is round. Gary is not blue. Harry is quiet. Blue things are not nice. All blue things are nice. Round things are nice. Quiet things are round. Round things are not big. If something is quiet and not big then it is smart.
Charlie is round.
("Charlie" "is" "round" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Blue things are not nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "-"))
All blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Quiet things are round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
Round things are not big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "-"))
If something is quiet and not big then it is smart.
((("something" "is" "quiet" "+") ("something" "is" "big" "~")) -> ("something" "is" "smart" "+"))
Harry is quiet.
True
1
proof
[(triple3)]
("Harry" "is" "quiet" "+")
triple3
Harry is not quiet.
False
1
inv-proof
[(triple3)]
("Harry" "is" "quiet" "-")
triple3
Harry is round.
True
2
proof
[(((triple3) -> rule4))]
("Harry" "is" "round" "+")
((triple3) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Harry is not big.
True
3
proof
[(((((triple3) -> rule4)) -> rule5))]
("Harry" "is" "big" "-")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule5))]
("Harry" "is" "big" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is smart.
True
5
proof
[(((triple3 ((((triple3) -> rule4)) -> rule5)) -> rule6))]
("Harry" "is" "smart" "+")
((triple3 ((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not big.
("Harry" "is" "big" "-")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is not smart.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule4)) -> rule5)) -> rule6))]
("Harry" "is" "smart" "-")
((triple3 ((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not big.
("Harry" "is" "big" "-")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "smart" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "smart" "+")
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is nice.
Unknown
rconc
[@2: Gary is nice.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Gary" "is" "nice" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is round.[(triple1)] Gary is not blue.[(triple2)] Harry is quiet.[(triple3)] @1: Charlie is nice.[(((triple1) -> rule3))] Charlie is not big.[(((triple1) -> rule5))] Harry is round.[(((triple3) -> rule4))] @2: Harry is nice.[(((((triple3) -> rule4)) -> rule3))] Harry is not big.[(((((triple3) -> rule4)) -> rule5))] @3: Harry is smart.[(((triple3 ((((triple3) -> rule4)) -> rule5)) -> rule6))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Gary is not blue.
("Gary" "is" "blue" "-")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not big.
("Charlie" "is" "big" "-")
((triple1) -> (rule5 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple3) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not big.
("Harry" "is" "big" "-")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((triple3 ((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not big.
("Harry" "is" "big" "-")
int2
Harry is round.
("Harry" "is" "round" "+")
int3