Bob is cold. Bob is green. Bob is nice. Bob is red. Bob is not smart. Charlie is blue. Charlie is cold. Charlie is green. Charlie is nice. Charlie is red. Charlie is smart. Charlie is young. Smart, young things are red. If something is young and green then it is nice. All nice things are blue.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Smart, young things are red.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something is young and green then it is nice.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
All nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Charlie is cold.
True
1
proof
[(triple7)]
("Charlie" "is" "cold" "+")
triple7
Charlie is not smart.
False
1
inv-proof
[(triple11)]
("Charlie" "is" "smart" "-")
triple11
Bob is blue.
True
2
proof
[(((triple3) -> rule3))]
("Bob" "is" "blue" "+")
((triple3) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple3) -> rule3))]
("Bob" "is" "blue" "-")
((triple3) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
@0: Bob is cold.[(triple1)] Bob is green.[(triple2)] Bob is nice.[(triple3)] Bob is not smart.[(triple5)] Bob is red.[(triple4)] Charlie is blue.[(triple6 OR ((triple9) -> rule3) OR ((((triple12 triple8) -> rule2)) -> rule3))] Charlie is cold.[(triple7)] Charlie is green.[(triple8)] Charlie is nice.[(triple9 OR ((triple12 triple8) -> rule2))] Charlie is red.[(triple10 OR ((triple11 triple12) -> rule1))] Charlie is smart.[(triple11)] Charlie is young.[(triple12)] @1: Bob is blue.[(((triple3) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is not smart.
("Bob" "is" "smart" "-")
triple5
Bob is red.
("Bob" "is" "red" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
((triple9) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple12 triple8) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
triple8
Charlie is nice.
("Charlie" "is" "nice" "+")
triple9
((triple12 triple8) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple10
((triple11 triple12) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple11
Charlie is young.
("Charlie" "is" "young" "+")
triple12
Bob is blue.
("Bob" "is" "blue" "+")
((triple3) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1