Dave is quiet. Erin is big. Erin is quiet. Erin is red. Erin is rough. Erin is young. Fiona is big. Fiona is quiet. Fiona is red. Fiona is smart. Quiet people are smart. Young, round people are big. Quiet people are young. If someone is big then they are young. If someone is smart and quiet then they are round. If Fiona is big and Fiona is smart then Fiona is rough. Smart people are rough. If Dave is young and Dave is smart then Dave is round.
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
Young, round people are big.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
Quiet people are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If someone is big then they are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is smart and quiet then they are round.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If Fiona is big and Fiona is smart then Fiona is rough.
((("Fiona" "is" "big" "+") ("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "rough" "+"))
Smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If Dave is young and Dave is smart then Dave is round.
((("Dave" "is" "young" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "round" "+"))
Fiona is red.
True
1
proof
[(triple9)]
("Fiona" "is" "red" "+")
triple9
Erin is not red.
False
1
inv-proof
[(triple4)]
("Erin" "is" "red" "-")
triple4
Dave is smart.
True
2
proof
[(((triple1) -> rule1))]
("Dave" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple3) -> rule1))]
("Erin" "is" "smart" "-")
((triple3) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
True
4
proof
[(((((triple3) -> rule1) triple3) -> rule5))]
("Erin" "is" "round" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not round.
False
4
inv-proof
[(((((triple3) -> rule1) triple3) -> rule5))]
("Erin" "is" "round" "-")
((((triple3) -> (rule1 % int2)) triple3) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Dave is big.
True
7
proof
[(((((triple1) -> rule3) ((((triple1) -> rule1) triple1) -> rule5)) -> rule2) OR ((((triple1) -> rule3) ((((triple1) -> rule3) ((triple1) -> rule1)) -> rule8)) -> rule2))]
("Dave" "is" "big" "+")
((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule1 % int3)) triple1) -> (rule5 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule3 % int4)) ((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is not big.
False
7
inv-proof
[(((((triple1) -> rule3) ((((triple1) -> rule1) triple1) -> rule5)) -> rule2) OR ((((triple1) -> rule3) ((((triple1) -> rule3) ((triple1) -> rule1)) -> rule8)) -> rule2))]
("Dave" "is" "big" "-")
((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule1 % int3)) triple1) -> (rule5 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule3 % int4)) ((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
@0: Dave is quiet.[(triple1)] Erin is big.[(triple2 OR ((triple6 ((((triple3) -> rule1) triple3) -> rule5)) -> rule2) OR ((((triple3) -> rule3) ((((triple3) -> rule1) triple3) -> rule5)) -> rule2))] Erin is quiet.[(triple3)] Erin is red.[(triple4)] Erin is rough.[(triple5 OR ((((triple3) -> rule1)) -> rule7))] Erin is young.[(triple6 OR ((triple2) -> rule4) OR ((triple3) -> rule3))] Fiona is big.[(triple7 OR ((((triple8) -> rule3) ((triple10 triple8) -> rule5)) -> rule2) OR ((((triple8) -> rule3) ((((triple8) -> rule1) triple8) -> rule5)) -> rule2))] Fiona is quiet.[(triple8)] Fiona is red.[(triple9)] Fiona is smart.[(triple10 OR ((triple8) -> rule1))] @1: Dave is smart.[(((triple1) -> rule1))] Dave is young.[(((triple1) -> rule3))] Erin is smart.[(((triple3) -> rule1))] Fiona is rough.[(((triple10) -> rule7) OR ((triple7 triple10) -> rule6) OR ((((triple8) -> rule1)) -> rule7) OR ((triple7 ((triple8) -> rule1)) -> rule6) OR ((((((triple8) -> rule3) ((triple10 triple8) -> rule5)) -> rule2) triple10) -> rule6) OR ((((((triple8) -> rule3) ((triple10 triple8) -> rule5)) -> rule2) ((triple8) -> rule1)) -> rule6) OR ((((((triple8) -> rule3) ((((triple8) -> rule1) triple8) -> rule5)) -> rule2) triple10) -> rule6) OR ((((((triple8) -> rule3) ((((triple8) -> rule1) triple8) -> rule5)) -> rule2) ((triple8) -> rule1)) -> rule6))] Fiona is round.[(((triple10 triple8) -> rule5) OR ((((triple8) -> rule1) triple8) -> rule5))] Fiona is young.[(((triple7) -> rule4) OR ((triple8) -> rule3))] @2: Dave is rough.[(((((triple1) -> rule1)) -> rule7))] Dave is round.[(((((triple1) -> rule1) triple1) -> rule5) OR ((((triple1) -> rule3) ((triple1) -> rule1)) -> rule8))] Erin is round.[(((((triple3) -> rule1) triple3) -> rule5))] @3: Dave is big.[(((((triple1) -> rule3) ((((triple1) -> rule1) triple1) -> rule5)) -> rule2) OR ((((triple1) -> rule3) ((((triple1) -> rule3) ((triple1) -> rule1)) -> rule8)) -> rule2))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
((triple6 ((((triple3) -> (rule1 % int3)) triple3) -> (rule5 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((triple3) -> (rule3 % int4)) ((((triple3) -> (rule1 % int3)) triple3) -> (rule5 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple4
Erin is rough.
("Erin" "is" "rough" "+")
triple5
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple6
((triple2) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple3) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
triple7
((((triple8) -> (rule3 % int3)) ((triple10 triple8) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
((((triple8) -> (rule3 % int4)) ((((triple8) -> (rule1 % int3)) triple8) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple8
Fiona is red.
("Fiona" "is" "red" "+")
triple9
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
((triple8) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple1) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple10) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((triple7 triple10) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((triple7 ((triple8) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((((triple8) -> (rule3 % int4)) ((triple10 triple8) -> (rule5 % int3))) -> (rule2 % int2)) triple10) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
int4
((((((triple8) -> (rule3 % int5)) ((triple10 triple8) -> (rule5 % int4))) -> (rule2 % int3)) ((triple8) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Fiona is young.
("Fiona" "is" "young" "+")
int5
((((((triple8) -> (rule3 % int5)) ((((triple8) -> (rule1 % int4)) triple8) -> (rule5 % int3))) -> (rule2 % int2)) triple10) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is young.
("Fiona" "is" "young" "+")
int5
((((((triple8) -> (rule3 % int5)) ((((triple8) -> (rule1 % int4)) triple8) -> (rule5 % int3))) -> (rule2 % int2)) ((triple8) -> (rule1 % int4))) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is young.
("Fiona" "is" "young" "+")
int5
Fiona is round.
("Fiona" "is" "round" "+")
((triple10 triple8) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple8) -> (rule1 % int2)) triple8) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((triple7) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
((triple8) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple1) -> (rule3 % int3)) ((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule1 % int3)) triple1) -> (rule5 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule3 % int4)) ((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4