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