Charlie is kind. Erin is smart. Gary is blue. Harry is quiet. If Gary is kind then Gary is round. If someone is green then they are round. If Charlie is round then Charlie is green. If someone is smart and round then they are blue. If someone is smart and green then they are round. All smart people are green.
Charlie is kind.
("Charlie" "is" "kind" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Gary is kind then Gary is round.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "round" "+"))
If someone is green then they are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If Charlie is round then Charlie is green.
((("Charlie" "is" "round" "+")) -> ("Charlie" "is" "green" "+"))
If someone is smart and round then they are blue.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is smart and green then they are round.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
All smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
Erin is smart.
True
1
proof
[(triple2)]
("Erin" "is" "smart" "+")
triple2
Charlie is not kind.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "kind" "-")
triple1
Erin is green.
True
2
proof
[(((triple2) -> rule6))]
("Erin" "is" "green" "+")
((triple2) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple2) -> rule6))]
("Erin" "is" "green" "-")
((triple2) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is round.
True
3
proof
[(((((triple2) -> rule6)) -> rule2) OR ((triple2 ((triple2) -> rule6)) -> rule5))]
("Erin" "is" "round" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((triple2 ((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule2) OR ((triple2 ((triple2) -> rule6)) -> rule5))]
("Erin" "is" "round" "-")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((triple2 ((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is blue.
True
5
proof
[(((triple2 ((((triple2) -> rule6)) -> rule2)) -> rule4) OR ((triple2 ((triple2 ((triple2) -> rule6)) -> rule5)) -> rule4))]
("Erin" "is" "blue" "+")
((triple2 ((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((triple2 ((triple2 ((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is not blue.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule6)) -> rule2)) -> rule4) OR ((triple2 ((triple2 ((triple2) -> rule6)) -> rule5)) -> rule4))]
("Erin" "is" "blue" "-")
((triple2 ((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((triple2 ((triple2 ((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "green" "-")
Charlie is round.
Unknown
rconc
[@3: Charlie is round.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule5 <- FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "blue" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "blue" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Charlie is kind.[(triple1)] Erin is smart.[(triple2)] Gary is blue.[(triple3)] Harry is quiet.[(triple4)] @1: Erin is green.[(((triple2) -> rule6))] @2: Erin is round.[(((((triple2) -> rule6)) -> rule2) OR ((triple2 ((triple2) -> rule6)) -> rule5))] @3: Erin is blue.[(((triple2 ((((triple2) -> rule6)) -> rule2)) -> rule4) OR ((triple2 ((triple2 ((triple2) -> rule6)) -> rule5)) -> rule4))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Erin is green.
("Erin" "is" "green" "+")
((triple2) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((triple2 ((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((triple2 ((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((triple2 ((triple2 ((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3