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