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