Dave is big. Dave is cold. Dave is green. Dave is kind. Dave is nice. Dave is round. Dave is smart. Erin is big. Erin is cold. Erin is green. Erin is kind. Erin is nice. If Erin is cold then Erin is round. If Erin is green then Erin is round. All round, nice things are smart. If Erin is kind and Erin is smart then Erin is round. Smart, big things are green. If Erin is cold then Erin is nice.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
If Erin is cold then Erin is round.
((("Erin" "is" "cold" "+")) -> ("Erin" "is" "round" "+"))
If Erin is green then Erin is round.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "round" "+"))
All round, nice things are smart.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If Erin is kind and Erin is smart then Erin is round.
((("Erin" "is" "kind" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "round" "+"))
Smart, big things are green.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If Erin is cold then Erin is nice.
((("Erin" "is" "cold" "+")) -> ("Erin" "is" "nice" "+"))
Dave is cold.
True
1
proof
[(triple2)]
("Dave" "is" "cold" "+")
triple2
Dave is not cold.
False
1
inv-proof
[(triple2)]
("Dave" "is" "cold" "-")
triple2
Erin is round.
True
2
proof
[(((triple10) -> rule2) OR ((triple9) -> rule1))]
("Erin" "is" "round" "+")
((triple10) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple9) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple10) -> rule2) OR ((triple9) -> rule1))]
("Erin" "is" "round" "-")
((triple10) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple9) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
True
4
proof
[(((((triple10) -> rule2) triple12) -> rule3) OR ((((triple9) -> rule1) triple12) -> rule3) OR ((((triple10) -> rule2) ((triple9) -> rule6)) -> rule3) OR ((((triple9) -> rule1) ((triple9) -> rule6)) -> rule3))]
("Erin" "is" "smart" "+")
((((triple10) -> (rule2 % int2)) triple12) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple9) -> (rule1 % int2)) triple12) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple10) -> (rule2 % int3)) ((triple9) -> (rule6 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((triple9) -> (rule1 % int3)) ((triple9) -> (rule6 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not smart.
False
4
inv-proof
[(((((triple10) -> rule2) triple12) -> rule3) OR ((((triple9) -> rule1) triple12) -> rule3) OR ((((triple10) -> rule2) ((triple9) -> rule6)) -> rule3) OR ((((triple9) -> rule1) ((triple9) -> rule6)) -> rule3))]
("Erin" "is" "smart" "-")
((((triple10) -> (rule2 % int2)) triple12) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple9) -> (rule1 % int2)) triple12) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple10) -> (rule2 % int3)) ((triple9) -> (rule6 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((triple9) -> (rule1 % int3)) ((triple9) -> (rule6 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
@0: Dave is big.[(triple1)] Dave is cold.[(triple2)] Dave is green.[(triple3 OR ((triple7 triple1) -> rule5) OR ((((triple6 triple5) -> rule3) triple1) -> rule5))] Dave is kind.[(triple4)] Dave is nice.[(triple5)] Dave is round.[(triple6)] Dave is smart.[(triple7 OR ((triple6 triple5) -> rule3))] Erin is big.[(triple8)] Erin is cold.[(triple9)] Erin is green.[(triple10 OR ((((((triple9) -> rule1) triple12) -> rule3) triple8) -> rule5) OR ((((((triple9) -> rule1) ((triple9) -> rule6)) -> rule3) triple8) -> rule5))] Erin is kind.[(triple11)] Erin is nice.[(triple12 OR ((triple9) -> rule6))] @1: Erin is round.[(((triple10) -> rule2) OR ((triple9) -> rule1))] @2: Erin is smart.[(((((triple10) -> rule2) triple12) -> rule3) OR ((((triple9) -> rule1) triple12) -> rule3) OR ((((triple10) -> rule2) ((triple9) -> rule6)) -> rule3) OR ((((triple9) -> rule1) ((triple9) -> rule6)) -> rule3))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
((triple7 triple1) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple6 triple5) -> (rule3 % int2)) triple1) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
((triple6 triple5) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple8
Erin is cold.
("Erin" "is" "cold" "+")
triple9
Erin is green.
("Erin" "is" "green" "+")
triple10
((((((triple9) -> (rule1 % int3)) triple12) -> (rule3 % int2)) triple8) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((((triple9) -> (rule1 % int4)) ((triple9) -> (rule6 % int3))) -> (rule3 % int2)) triple8) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
triple11
Erin is nice.
("Erin" "is" "nice" "+")
triple12
((triple9) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple10) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple9) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((((triple10) -> (rule2 % int2)) triple12) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple9) -> (rule1 % int2)) triple12) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple10) -> (rule2 % int3)) ((triple9) -> (rule6 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((triple9) -> (rule1 % int3)) ((triple9) -> (rule6 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3