Bob is cold. Bob is furry. Bob is green. Bob is kind. Bob is nice. Bob is rough. Fiona is cold. Fiona is furry. Fiona is green. Fiona is nice. If Bob is nice then Bob is furry. All rough people are green. If someone is kind then they are quiet. If someone is green and cold then they are quiet. Green people are quiet. Furry people are 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 rough.
("Bob" "is" "rough" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
If Bob is nice then Bob is furry.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "furry" "+"))
All rough people are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If someone is kind then they are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If someone is green and cold then they are quiet.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
Green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
Furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Bob is furry.
True
1
proof
[(triple2 OR ((triple5) -> rule1))]
("Bob" "is" "furry" "+")
triple2
((triple5) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not kind.
False
1
inv-proof
[(triple4 OR ((triple2) -> rule6) OR ((((triple5) -> rule1)) -> rule6))]
("Bob" "is" "kind" "-")
triple4
((triple2) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
@0: Bob is cold.[(triple1)] Bob is furry.[(triple2 OR ((triple5) -> rule1))] Bob is green.[(triple3 OR ((triple6) -> rule2))] Bob is kind.[(triple4 OR ((triple2) -> rule6) OR ((((triple5) -> rule1)) -> rule6))] Bob is nice.[(triple5)] Bob is rough.[(triple6)] Fiona is cold.[(triple7)] Fiona is furry.[(triple8)] Fiona is green.[(triple9)] Fiona is nice.[(triple10)] @1: Bob is quiet.[(((triple3) -> rule5) OR ((triple4) -> rule3) OR ((triple3 triple1) -> rule4) OR ((((triple2) -> rule6)) -> rule3) OR ((((triple6) -> rule2)) -> rule5) OR ((((triple6) -> rule2) triple1) -> rule4) OR ((((((triple5) -> rule1)) -> rule6)) -> rule3))] Fiona is kind.[(((triple8) -> rule6))] Fiona is quiet.[(((triple9) -> rule5) OR ((triple9 triple7) -> rule4) OR ((((triple8) -> rule6)) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple5) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple3
((triple6) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple4
((triple2) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
triple5
Bob is rough.
("Bob" "is" "rough" "+")
triple6
Fiona is cold.
("Fiona" "is" "cold" "+")
triple7
Fiona is furry.
("Fiona" "is" "furry" "+")
triple8
Fiona is green.
("Fiona" "is" "green" "+")
triple9
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple4) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple3 triple1) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple6) -> (rule2 % int2))) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple6) -> (rule2 % int2)) triple1) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((((triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple8) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple9) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((triple9 triple7) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple8) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2