Bob is cold. Bob is furry. Bob is green. Bob is kind. Bob is nice. Bob is red. Bob is round. Erin is cold. Erin is furry. Erin is green. Erin is kind. Erin is nice. Erin is red. Erin is round. If something is cold and kind then it is furry. If Erin is cold then Erin is red. If something is cold and round then it is red. All furry things are kind. All green things are furry. If Bob is cold then Bob is round. Red things are nice. If something is cold and green then it is kind.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
If something is cold and kind then it is furry.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
If Erin is cold then Erin is red.
((("Erin" "is" "cold" "+")) -> ("Erin" "is" "red" "+"))
If something is cold and round then it is red.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
All furry things are kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
All green things are furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
If Bob is cold then Bob is round.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "round" "+"))
Red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If something is cold and green then it is kind.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
Bob is furry.
True
1
proof
[(triple2 OR ((triple3) -> rule5) OR ((triple1 triple4) -> rule1) OR ((triple1 ((triple1 triple3) -> rule8)) -> rule1))]
("Bob" "is" "furry" "+")
triple2
((triple3) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple1 triple4) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple1 ((triple1 triple3) -> (rule8 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not round.
False
1
inv-proof
[(triple7 OR ((triple1) -> rule6))]
("Bob" "is" "round" "-")
triple7
((triple1) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
@0: Bob is cold.[(triple1)] Bob is furry.[(triple2 OR ((triple3) -> rule5) OR ((triple1 triple4) -> rule1) OR ((triple1 ((triple1 triple3) -> rule8)) -> rule1))] Bob is green.[(triple3)] Bob is kind.[(triple4 OR ((triple2) -> rule4) OR ((triple1 triple3) -> rule8) OR ((((triple3) -> rule5)) -> rule4))] Bob is nice.[(triple5 OR ((triple6) -> rule7) OR ((((triple1 triple7) -> rule3)) -> rule7) OR ((((triple1 ((triple1) -> rule6)) -> rule3)) -> rule7))] Bob is red.[(triple6 OR ((triple1 triple7) -> rule3) OR ((triple1 ((triple1) -> rule6)) -> rule3))] Bob is round.[(triple7 OR ((triple1) -> rule6))] Erin is cold.[(triple8)] Erin is furry.[(triple9 OR ((triple10) -> rule5) OR ((triple8 triple11) -> rule1) OR ((triple8 ((triple8 triple10) -> rule8)) -> rule1))] Erin is green.[(triple10)] Erin is kind.[(triple11 OR ((triple9) -> rule4) OR ((triple8 triple10) -> rule8) OR ((((triple10) -> rule5)) -> rule4))] Erin is nice.[(triple12 OR ((triple13) -> rule7) OR ((((triple8) -> rule2)) -> rule7) OR ((((triple8 triple14) -> rule3)) -> rule7))] Erin is red.[(triple13 OR ((triple8) -> rule2) OR ((triple8 triple14) -> rule3))] Erin is round.[(triple14)]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple3) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple1 triple4) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple1 ((triple1 triple3) -> (rule8 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
((triple2) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple1 triple3) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
triple5
((triple6) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple1 triple7) -> (rule3 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple1 ((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
triple6
((triple1 triple7) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple1 ((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
triple7
((triple1) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple8
Erin is furry.
("Erin" "is" "furry" "+")
triple9
((triple10) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple8 triple11) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple8 ((triple8 triple10) -> (rule8 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
triple10
Erin is kind.
("Erin" "is" "kind" "+")
triple11
((triple9) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple8 triple10) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
triple12
((triple13) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple8 triple14) -> (rule3 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple13
((triple8) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple8 triple14) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple14