Charlie is blue. Charlie is green. Charlie is quiet. Charlie is not rough. Charlie is smart. Charlie is white. Erin is green. Erin is quiet. Erin is rough. Erin is smart. Erin is not white. Erin is young. If something is quiet and young then it is blue. If something is quiet and young then it is blue. All smart, quiet things are young. If something is white and not quiet then it is young. Smart, blue things are young. If something is quiet and not green then it is not rough.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is not white.
("Erin" "is" "white" "-")
Erin is young.
("Erin" "is" "young" "+")
If something is quiet and young then it is blue.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something is quiet and young then it is blue.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
All smart, quiet things are young.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
If something is white and not quiet then it is young.
((("something" "is" "white" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "young" "+"))
Smart, blue things are young.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is quiet and not green then it is not rough.
((("something" "is" "quiet" "+") ("something" "is" "green" "~")) -> ("something" "is" "rough" "-"))
Erin is quiet.
True
1
proof
[(triple8)]
("Erin" "is" "quiet" "+")
triple8
Charlie is rough.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "rough" "+")
triple4
Charlie is young.
True
3
proof
[(((triple5 triple1) -> rule5) OR ((triple5 triple3) -> rule3))]
("Charlie" "is" "young" "+")
((triple5 triple1) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple5 triple3) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not young.
False
3
inv-proof
[(((triple5 triple1) -> rule5) OR ((triple5 triple3) -> rule3))]
("Charlie" "is" "young" "-")
((triple5 triple1) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple5 triple3) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
@0: Charlie is blue.[(triple1 OR ((triple3 ((triple5 triple3) -> rule3)) -> rule1) OR ((triple3 ((triple5 triple3) -> rule3)) -> rule2))] Charlie is green.[(triple2)] Charlie is not rough.[(triple4)] Charlie is quiet.[(triple3)] Charlie is smart.[(triple5)] Charlie is white.[(triple6)] Erin is green.[(triple7)] Erin is not white.[(triple11)] Erin is quiet.[(triple8)] Erin is rough.[(triple9)] Erin is smart.[(triple10)] Erin is young.[(triple12 OR ((triple10 triple8) -> rule3))] @1: Charlie is young.[(((triple5 triple1) -> rule5) OR ((triple5 triple3) -> rule3))] Erin is blue.[(((triple8 triple12) -> rule1) OR ((triple8 triple12) -> rule2) OR ((triple8 ((triple10 triple8) -> rule3)) -> rule1) OR ((triple8 ((triple10 triple8) -> rule3)) -> rule2))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple3 ((triple5 triple3) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((triple3 ((triple5 triple3) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Erin is green.
("Erin" "is" "green" "+")
triple7
Erin is not white.
("Erin" "is" "white" "-")
triple11
Erin is quiet.
("Erin" "is" "quiet" "+")
triple8
Erin is rough.
("Erin" "is" "rough" "+")
triple9
Erin is smart.
("Erin" "is" "smart" "+")
triple10
Erin is young.
("Erin" "is" "young" "+")
triple12
((triple10 triple8) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple5 triple1) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple5 triple3) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple8 triple12) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple8 triple12) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple8 ((triple10 triple8) -> (rule3 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((triple8 ((triple10 triple8) -> (rule3 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2