Erin is quiet. Gary is young. Harry is white. If someone is kind and green then they are smart. Kind people are white. Red people are young. Young people are green. If someone is quiet and young then they are white. All white people are red. If Erin is green then Erin is smart. All smart people are young.
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is kind and green then they are smart.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
Kind people are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
Young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
If someone is quiet and young then they are white.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
All white people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
If Erin is green then Erin is smart.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "smart" "+"))
All smart people are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
Erin is quiet.
True
1
proof
[(triple1)]
("Erin" "is" "quiet" "+")
triple1
Erin is not quiet.
False
1
inv-proof
[(triple1)]
("Erin" "is" "quiet" "-")
triple1
Gary is green.
True
2
proof
[(((triple2) -> rule4))]
("Gary" "is" "green" "+")
((triple2) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple3) -> rule6))]
("Harry" "is" "red" "-")
((triple3) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
True
3
proof
[(((((triple3) -> rule6)) -> rule3))]
("Harry" "is" "young" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not young.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule3))]
("Harry" "is" "young" "-")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is green.
True
4
proof
[(((((((triple3) -> rule6)) -> rule3)) -> rule4))]
("Harry" "is" "green" "+")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is not green.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule3)) -> rule4))]
("Harry" "is" "green" "-")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Erin is not white.
Unknown
inv-rconc
[@7: Erin is white.[CWA. Example of deepest failure = (rule5 <- rule8 <- rule7 <- rule4 <- rule3 <- rule6 <- rule2 <- FAIL)]]
("Erin" "is" "white" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "white" "+")
Gary is not red.
Unknown
inv-rconc
[@2: Gary is red.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Gary" "is" "red" "-")
Harry is smart.
Unknown
rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "smart" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Erin is quiet.[(triple1)] Gary is young.[(triple2)] Harry is white.[(triple3)] @1: Gary is green.[(((triple2) -> rule4))] Harry is red.[(((triple3) -> rule6))] @2: Harry is young.[(((((triple3) -> rule6)) -> rule3))] @3: Harry is green.[(((((((triple3) -> rule6)) -> rule3)) -> rule4))]
Erin is quiet.
("Erin" "is" "quiet" "+")
triple1
Gary is young.
("Gary" "is" "young" "+")
triple2
Harry is white.
("Harry" "is" "white" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
((triple2) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple3) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3