Erin is blue. Erin is kind. Erin is nice. Erin is smart. Erin is white. Erin is young. Harry is smart. If Harry is smart and Harry is white then Harry is furry. If Erin is furry then Erin is white. All white people are blue. Smart people are white. All furry people are kind. If Harry is blue and Harry is smart then Harry is young.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Harry is smart and Harry is white then Harry is furry.
((("Harry" "is" "smart" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "furry" "+"))
If Erin is furry then Erin is white.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "white" "+"))
All white people are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
Smart people are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
All furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If Harry is blue and Harry is smart then Harry is young.
((("Harry" "is" "blue" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "young" "+"))
Erin is blue.
True
1
proof
[(triple1 OR ((triple5) -> rule3) OR ((((triple4) -> rule4)) -> rule3))]
("Erin" "is" "blue" "+")
triple1
((triple5) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is not blue.
False
1
inv-proof
[(triple1 OR ((triple5) -> rule3) OR ((((triple4) -> rule4)) -> rule3))]
("Erin" "is" "blue" "-")
triple1
((triple5) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Harry is white.
True
2
proof
[(((triple7) -> rule4))]
("Harry" "is" "white" "+")
((triple7) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple7) -> rule4))]
("Harry" "is" "white" "-")
((triple7) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
True
3
proof
[(((((triple7) -> rule4)) -> rule3))]
("Harry" "is" "blue" "+")
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not furry.
False
4
inv-proof
[(((triple7 ((triple7) -> rule4)) -> rule1))]
("Harry" "is" "furry" "-")
((triple7 ((triple7) -> (rule4 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
True
5
proof
[(((((((triple7) -> rule4)) -> rule3) triple7) -> rule6))]
("Harry" "is" "young" "+")
((((((triple7) -> (rule4 % int3))) -> (rule3 % int2)) triple7) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is not young.
False
5
inv-proof
[(((((((triple7) -> rule4)) -> rule3) triple7) -> rule6))]
("Harry" "is" "young" "-")
((((((triple7) -> (rule4 % int3))) -> (rule3 % int2)) triple7) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Erin is blue.[(triple1 OR ((triple5) -> rule3) OR ((((triple4) -> rule4)) -> rule3))] Erin is kind.[(triple2)] Erin is nice.[(triple3)] Erin is smart.[(triple4)] Erin is white.[(triple5 OR ((triple4) -> rule4))] Erin is young.[(triple6)] Harry is smart.[(triple7)] @1: Harry is white.[(((triple7) -> rule4))] @2: Harry is blue.[(((((triple7) -> rule4)) -> rule3))] Harry is furry.[(((triple7 ((triple7) -> rule4)) -> rule1))] @3: Harry is kind.[(((((triple7 ((triple7) -> rule4)) -> rule1)) -> rule5))] Harry is young.[(((((((triple7) -> rule4)) -> rule3) triple7) -> rule6))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
((triple5) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
triple4
Erin is white.
("Erin" "is" "white" "+")
triple5
((triple4) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Harry is white.
("Harry" "is" "white" "+")
((triple7) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((triple7 ((triple7) -> (rule4 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple7 ((triple7) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
((((((triple7) -> (rule4 % int3))) -> (rule3 % int2)) triple7) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3