Charlie is nice. Charlie is quiet. Charlie is young. Dave is big. Dave is nice. Dave is quiet. Dave is not rough. Dave is round. Dave is smart. Dave is young. Erin is big. Erin is nice. Erin is rough. Erin is round. Erin is smart. Erin is young. If Charlie is young and Charlie is smart then Charlie is round. If someone is quiet then they are big. All rough, nice people are big. Nice, big people are smart. All young people are smart. Round, young people are quiet. All rough people are quiet. If Erin is nice and Erin is not round then Erin is young.
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
If Charlie is young and Charlie is smart then Charlie is round.
((("Charlie" "is" "young" "+") ("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "round" "+"))
If someone is quiet then they are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
All rough, nice people are big.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
Nice, big people are smart.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
All young people are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
Round, young people are quiet.
((("someone" "is" "round" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
All rough people are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If Erin is nice and Erin is not round then Erin is young.
((("Erin" "is" "nice" "+") ("Erin" "is" "round" "~")) -> ("Erin" "is" "young" "+"))
Dave is quiet.
True
1
proof
[(triple6 OR ((triple8 triple10) -> rule6))]
("Dave" "is" "quiet" "+")
triple6
((triple8 triple10) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not young.
False
1
inv-proof
[(triple10)]
("Dave" "is" "young" "-")
triple10
Erin is quiet.
True
2
proof
[(((triple13) -> rule7) OR ((triple14 triple16) -> rule6))]
("Erin" "is" "quiet" "+")
((triple13) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple14 triple16) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple2) -> rule2) OR ((((((triple3 ((triple3) -> rule5)) -> rule1) triple3) -> rule6)) -> rule2))]
("Charlie" "is" "big" "-")
((triple2) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((((triple3 ((triple3) -> (rule5 % int4))) -> (rule1 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Charlie is round.
True
4
proof
[(((triple3 ((triple3) -> rule5)) -> rule1) OR ((triple3 ((triple1 ((triple2) -> rule2)) -> rule4)) -> rule1))]
("Charlie" "is" "round" "+")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
((triple3 ((triple1 ((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not round.
False
4
inv-proof
[(((triple3 ((triple3) -> rule5)) -> rule1) OR ((triple3 ((triple1 ((triple2) -> rule2)) -> rule4)) -> rule1))]
("Charlie" "is" "round" "-")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
((triple3 ((triple1 ((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
@0: Charlie is nice.[(triple1)] Charlie is quiet.[(triple2 OR ((((triple3 ((triple3) -> rule5)) -> rule1) triple3) -> rule6))] Charlie is young.[(triple3)] Dave is big.[(triple4 OR ((triple6) -> rule2) OR ((((triple8 triple10) -> rule6)) -> rule2))] Dave is nice.[(triple5)] Dave is not rough.[(triple7)] Dave is quiet.[(triple6 OR ((triple8 triple10) -> rule6))] Dave is round.[(triple8)] Dave is smart.[(triple9 OR ((triple10) -> rule5) OR ((triple5 triple4) -> rule4) OR ((triple5 ((triple6) -> rule2)) -> rule4) OR ((triple5 ((((triple8 triple10) -> rule6)) -> rule2)) -> rule4))] Dave is young.[(triple10)] Erin is big.[(triple11 OR ((triple13 triple12) -> rule3) OR ((((triple13) -> rule7)) -> rule2) OR ((((triple14 triple16) -> rule6)) -> rule2))] Erin is nice.[(triple12)] Erin is rough.[(triple13)] Erin is round.[(triple14)] Erin is smart.[(triple15 OR ((triple16) -> rule5) OR ((triple12 triple11) -> rule4) OR ((triple12 ((triple13 triple12) -> rule3)) -> rule4) OR ((triple12 ((((triple13) -> rule7)) -> rule2)) -> rule4) OR ((triple12 ((((triple14 triple16) -> rule6)) -> rule2)) -> rule4))] Erin is young.[(triple16)] @1: Charlie is big.[(((triple2) -> rule2) OR ((((((triple3 ((triple3) -> rule5)) -> rule1) triple3) -> rule6)) -> rule2))] Charlie is smart.[(((triple3) -> rule5) OR ((triple1 ((triple2) -> rule2)) -> rule4))] Erin is quiet.[(((triple13) -> rule7) OR ((triple14 triple16) -> rule6))] @2: Charlie is round.[(((triple3 ((triple3) -> rule5)) -> rule1) OR ((triple3 ((triple1 ((triple2) -> rule2)) -> rule4)) -> rule1))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
((((triple3 ((triple3) -> (rule5 % int3))) -> (rule1 % int2)) triple3) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
((triple6) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple8 triple10) -> (rule6 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is not rough.
("Dave" "is" "rough" "-")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
((triple8 triple10) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple8
Dave is smart.
("Dave" "is" "smart" "+")
triple9
((triple10) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple5 triple4) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple5 ((triple6) -> (rule2 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((triple5 ((((triple8 triple10) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
triple10
Erin is big.
("Erin" "is" "big" "+")
triple11
((triple13 triple12) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple13) -> (rule7 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple14 triple16) -> (rule6 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
triple12
Erin is rough.
("Erin" "is" "rough" "+")
triple13
Erin is round.
("Erin" "is" "round" "+")
triple14
Erin is smart.
("Erin" "is" "smart" "+")
triple15
((triple16) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple12 triple11) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple12 ((triple13 triple12) -> (rule3 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((triple12 ((((triple13) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((triple12 ((((triple14 triple16) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
triple16
Charlie is big.
("Charlie" "is" "big" "+")
((triple2) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((((triple3 ((triple3) -> (rule5 % int4))) -> (rule1 % int3)) triple3) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple3) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple1 ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple13) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple14 triple16) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
((triple3 ((triple1 ((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3