Dave is big. Dave is cold. Dave is furry. Dave is kind. Dave is quiet. Dave is smart. Dave is young. Erin is big. Erin is cold. Erin is kind. All quiet, young people are furry. If someone is smart then they are furry. If Erin is big then Erin is smart. If Dave is quiet and Dave is big then Dave is kind. If someone is furry and cold then they are young. If Dave is kind then Dave is young.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
All quiet, young people are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
If someone is smart then they are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If Erin is big then Erin is smart.
((("Erin" "is" "big" "+")) -> ("Erin" "is" "smart" "+"))
If Dave is quiet and Dave is big then Dave is kind.
((("Dave" "is" "quiet" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "kind" "+"))
If someone is furry and cold then they are young.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If Dave is kind then Dave is young.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "young" "+"))
Dave is cold.
True
1
proof
[(triple2)]
("Dave" "is" "cold" "+")
triple2
Dave is not kind.
False
1
inv-proof
[(triple4 OR ((triple5 triple1) -> rule4))]
("Dave" "is" "kind" "-")
triple4
((triple5 triple1) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Erin is smart.
True
2
proof
[(((triple8) -> rule3))]
("Erin" "is" "smart" "+")
((triple8) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple8) -> rule3))]
("Erin" "is" "smart" "-")
((triple8) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
True
3
proof
[(((((triple8) -> rule3)) -> rule2))]
("Erin" "is" "furry" "+")
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not furry.
False
3
inv-proof
[(((((triple8) -> rule3)) -> rule2))]
("Erin" "is" "furry" "-")
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is young.
True
5
proof
[(((((((triple8) -> rule3)) -> rule2) triple9) -> rule5))]
("Erin" "is" "young" "+")
((((((triple8) -> (rule3 % int3))) -> (rule2 % int2)) triple9) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not young.
False
5
inv-proof
[(((((((triple8) -> rule3)) -> rule2) triple9) -> rule5))]
("Erin" "is" "young" "-")
((((((triple8) -> (rule3 % int3))) -> (rule2 % int2)) triple9) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
@0: Dave is big.[(triple1)] Dave is cold.[(triple2)] Dave is furry.[(triple3 OR ((triple6) -> rule2) OR ((triple5 triple7) -> rule1) OR ((triple5 ((triple4) -> rule6)) -> rule1) OR ((triple5 ((((triple5 triple1) -> rule4)) -> rule6)) -> rule1))] Dave is kind.[(triple4 OR ((triple5 triple1) -> rule4))] Dave is quiet.[(triple5)] Dave is smart.[(triple6)] Dave is young.[(triple7 OR ((triple4) -> rule6) OR ((triple3 triple2) -> rule5) OR ((((triple5 triple1) -> rule4)) -> rule6) OR ((((triple6) -> rule2) triple2) -> rule5))] Erin is big.[(triple8)] Erin is cold.[(triple9)] Erin is kind.[(triple10)] @1: Erin is smart.[(((triple8) -> rule3))] @2: Erin is furry.[(((((triple8) -> rule3)) -> rule2))] @3: Erin is young.[(((((((triple8) -> rule3)) -> rule2) triple9) -> rule5))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
((triple6) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple5 triple7) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple5 ((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((triple5 ((((triple5 triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
((triple5 triple1) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
((triple4) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple3 triple2) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple5 triple1) -> (rule4 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple6) -> (rule2 % int2)) triple2) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
triple8
Erin is cold.
("Erin" "is" "cold" "+")
triple9
Erin is kind.
("Erin" "is" "kind" "+")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
((triple8) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((((((triple8) -> (rule3 % int3))) -> (rule2 % int2)) triple9) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3