Bob is cold. Bob is furry. Bob is quiet. Bob is rough. Bob is not smart. Bob is white. Fiona is big. Fiona is cold. Fiona is furry. Fiona is quiet. Fiona is smart. Fiona is white. Big, smart things are furry. All rough, white things are furry. If something is white and cold then it is big. All furry, white things are big. If something is big then it is white. If something is white then it is cold. Cold, rough things are quiet. All rough things are quiet.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Bob is white.
("Bob" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Big, smart things are furry.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
All rough, white things are furry.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If something is white and cold then it is big.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
All furry, white things are big.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If something is big then it is white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If something is white then it is cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Cold, rough things are quiet.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
All rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Fiona is quiet.
True
1
proof
[(triple10)]
("Fiona" "is" "quiet" "+")
triple10
Fiona is not furry.
False
1
inv-proof
[(triple9 OR ((triple7 triple11) -> rule1) OR ((((triple12 triple8) -> rule3) triple11) -> rule1) OR ((((triple12 ((triple12) -> rule6)) -> rule3) triple11) -> rule1))]
("Fiona" "is" "furry" "-")
triple9
((triple7 triple11) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple12 triple8) -> (rule3 % int2)) triple11) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((triple12 ((triple12) -> (rule6 % int3))) -> (rule3 % int2)) triple11) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Bob is big.
True
3
proof
[(((triple2 triple6) -> rule4) OR ((triple6 triple1) -> rule3) OR ((triple6 ((triple6) -> rule6)) -> rule3) OR ((((triple4 triple6) -> rule2) triple6) -> rule4))]
("Bob" "is" "big" "+")
((triple2 triple6) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple6 triple1) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple6 ((triple6) -> (rule6 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple4 triple6) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is not big.
False
3
inv-proof
[(((triple2 triple6) -> rule4) OR ((triple6 triple1) -> rule3) OR ((triple6 ((triple6) -> rule6)) -> rule3) OR ((((triple4 triple6) -> rule2) triple6) -> rule4))]
("Bob" "is" "big" "-")
((triple2 triple6) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple6 triple1) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple6 ((triple6) -> (rule6 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple4 triple6) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
@0: Bob is cold.[(triple1 OR ((triple6) -> rule6))] Bob is furry.[(triple2 OR ((triple4 triple6) -> rule2))] Bob is not smart.[(triple5)] Bob is quiet.[(triple3 OR ((triple4) -> rule8) OR ((triple1 triple4) -> rule7) OR ((((triple6) -> rule6) triple4) -> rule7))] Bob is rough.[(triple4)] Bob is white.[(triple6)] Fiona is big.[(triple7 OR ((triple12 triple8) -> rule3) OR ((triple9 triple12) -> rule4) OR ((triple12 ((triple12) -> rule6)) -> rule3))] Fiona is cold.[(triple8 OR ((triple12) -> rule6) OR ((((triple7) -> rule5)) -> rule6))] Fiona is furry.[(triple9 OR ((triple7 triple11) -> rule1) OR ((((triple12 triple8) -> rule3) triple11) -> rule1) OR ((((triple12 ((triple12) -> rule6)) -> rule3) triple11) -> rule1))] Fiona is quiet.[(triple10)] Fiona is smart.[(triple11)] Fiona is white.[(triple12 OR ((triple7) -> rule5))] @1: Bob is big.[(((triple2 triple6) -> rule4) OR ((triple6 triple1) -> rule3) OR ((triple6 ((triple6) -> rule6)) -> rule3) OR ((((triple4 triple6) -> rule2) triple6) -> rule4))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((triple6) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple4 triple6) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not smart.
("Bob" "is" "smart" "-")
triple5
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((triple4) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple1 triple4) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple6) -> (rule6 % int2)) triple4) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple6
Fiona is big.
("Fiona" "is" "big" "+")
triple7
((triple12 triple8) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((triple9 triple12) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((triple12 ((triple12) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple8
((triple12) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((triple7) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple9
((triple7 triple11) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple12 triple8) -> (rule3 % int2)) triple11) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((triple12 ((triple12) -> (rule6 % int3))) -> (rule3 % int2)) triple11) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple10
Fiona is smart.
("Fiona" "is" "smart" "+")
triple11
Fiona is white.
("Fiona" "is" "white" "+")
triple12
((triple7) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((triple2 triple6) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple6 triple1) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple6 ((triple6) -> (rule6 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple4 triple6) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2