Bob is green. Bob is kind. Bob is red. Bob is round. Erin is big. Erin is green. Erin is kind. All nice people are kind. If Erin is kind and Erin is round then Erin is white. All nice, green people are not red. Big people are red. Red people are round. If someone is nice and not red then they are not white.
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
All nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If Erin is kind and Erin is round then Erin is white.
((("Erin" "is" "kind" "+") ("Erin" "is" "round" "+")) -> ("Erin" "is" "white" "+"))
All nice, green people are not red.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "-"))
Big people are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
Red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is nice and not red then they are not white.
((("someone" "is" "nice" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "white" "-"))
Bob is kind.
True
1
proof
[(triple2)]
("Bob" "is" "kind" "+")
triple2
Bob is not kind.
False
1
inv-proof
[(triple2)]
("Bob" "is" "kind" "-")
triple2
Erin is red.
True
2
proof
[(((triple5) -> rule4))]
("Erin" "is" "red" "+")
((triple5) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple5) -> rule4))]
("Erin" "is" "red" "-")
((triple5) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
True
3
proof
[(((((triple5) -> rule4)) -> rule5))]
("Erin" "is" "round" "+")
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple5) -> rule4)) -> rule5))]
("Erin" "is" "round" "-")
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is white.
True
5
proof
[(((triple7 ((((triple5) -> rule4)) -> rule5)) -> rule2))]
("Erin" "is" "white" "+")
((triple7 ((((triple5) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not white.
False
5
inv-proof
[(((triple7 ((((triple5) -> rule4)) -> rule5)) -> rule2))]
("Erin" "is" "white" "-")
((triple7 ((((triple5) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
@0: Bob is green.[(triple1)] Bob is kind.[(triple2)] Bob is red.[(triple3)] Bob is round.[(triple4 OR ((triple3) -> rule5))] Erin is big.[(triple5)] Erin is green.[(triple6)] Erin is kind.[(triple7)] @1: Erin is red.[(((triple5) -> rule4))] @2: Erin is round.[(((((triple5) -> rule4)) -> rule5))] @3: Erin is white.[(((triple7 ((((triple5) -> rule4)) -> rule5)) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
((triple3) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
Erin is kind.
("Erin" "is" "kind" "+")
triple7
Erin is red.
("Erin" "is" "red" "+")
((triple5) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((triple7 ((((triple5) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3