Charlie is furry. Charlie is kind. Charlie is quiet. Charlie is red. Charlie is smart. Charlie is young. Erin is quiet. Erin is red. Erin is smart. Erin is young. If something is quiet and kind then it is white. If something is red then it is kind. If Erin is quiet then Erin is red.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is quiet and kind then it is white.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If something is red then it is kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If Erin is quiet then Erin is red.
((("Erin" "is" "quiet" "+")) -> ("Erin" "is" "red" "+"))
Charlie is furry.
True
1
proof
[(triple1)]
("Charlie" "is" "furry" "+")
triple1
Erin is not quiet.
False
1
inv-proof
[(triple7)]
("Erin" "is" "quiet" "-")
triple7
Charlie is white.
True
3
proof
[(((triple3 triple2) -> rule1) OR ((triple3 ((triple4) -> rule2)) -> rule1))]
("Charlie" "is" "white" "+")
((triple3 triple2) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple3 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Erin is not kind.
False
2
inv-proof
[(((triple8) -> rule2) OR ((((triple7) -> rule3)) -> rule2))]
("Erin" "is" "kind" "-")
((triple8) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is white.
True
4
proof
[(((triple7 ((triple8) -> rule2)) -> rule1) OR ((triple7 ((((triple7) -> rule3)) -> rule2)) -> rule1))]
("Erin" "is" "white" "+")
((triple7 ((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((triple7 ((((triple7) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not white.
False
4
inv-proof
[(((triple7 ((triple8) -> rule2)) -> rule1) OR ((triple7 ((((triple7) -> rule3)) -> rule2)) -> rule1))]
("Erin" "is" "white" "-")
((triple7 ((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((triple7 ((((triple7) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
@0: Charlie is furry.[(triple1)] Charlie is kind.[(triple2 OR ((triple4) -> rule2))] Charlie is quiet.[(triple3)] Charlie is red.[(triple4)] Charlie is smart.[(triple5)] Charlie is young.[(triple6)] Erin is quiet.[(triple7)] Erin is red.[(triple8 OR ((triple7) -> rule3))] Erin is smart.[(triple9)] Erin is young.[(triple10)] @1: Charlie is white.[(((triple3 triple2) -> rule1) OR ((triple3 ((triple4) -> rule2)) -> rule1))] Erin is kind.[(((triple8) -> rule2) OR ((((triple7) -> rule3)) -> rule2))] @2: Erin is white.[(((triple7 ((triple8) -> rule2)) -> rule1) OR ((triple7 ((((triple7) -> rule3)) -> rule2)) -> rule1))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
((triple4) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Erin is red.
("Erin" "is" "red" "+")
triple8
((triple7) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple9
Erin is young.
("Erin" "is" "young" "+")
triple10
Charlie is white.
("Charlie" "is" "white" "+")
((triple3 triple2) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple3 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((triple8) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((triple7 ((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((triple7 ((((triple7) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3