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