Bob is cold. Bob is green. Bob is nice. Bob is red. Bob is rough. Bob is round. Bob is smart. Gary is cold. Gary is nice. Gary is red. Gary is rough. Gary is smart. If something is cold then it is round. If something is round then it is green. If something is cold and round then it is smart.
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 rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is round then it is green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something is cold and round then it is smart.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
Gary is rough.
True
1
proof
[(triple11)]
("Gary" "is" "rough" "+")
triple11
Bob is not smart.
False
1
inv-proof
[(triple7 OR ((triple1 triple6) -> rule3) OR ((triple1 ((triple1) -> rule1)) -> rule3))]
("Bob" "is" "smart" "-")
triple7
((triple1 triple6) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Gary is round.
True
2
proof
[(((triple8) -> rule1))]
("Gary" "is" "round" "+")
((triple8) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is not round.
False
2
inv-proof
[(((triple8) -> rule1))]
("Gary" "is" "round" "-")
((triple8) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
True
3
proof
[(((((triple8) -> rule1)) -> rule2))]
("Gary" "is" "green" "+")
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not green.
False
3
inv-proof
[(((((triple8) -> rule1)) -> rule2))]
("Gary" "is" "green" "-")
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
@0: Bob is cold.[(triple1)] Bob is green.[(triple2 OR ((triple6) -> rule2) OR ((((triple1) -> rule1)) -> rule2))] Bob is nice.[(triple3)] Bob is red.[(triple4)] Bob is rough.[(triple5)] Bob is round.[(triple6 OR ((triple1) -> rule1))] Bob is smart.[(triple7 OR ((triple1 triple6) -> rule3) OR ((triple1 ((triple1) -> rule1)) -> rule3))] Gary is cold.[(triple8)] Gary is nice.[(triple9)] Gary is red.[(triple10)] Gary is rough.[(triple11)] Gary is smart.[(triple12 OR ((triple8 ((triple8) -> rule1)) -> rule3))] @1: Gary is round.[(((triple8) -> rule1))] @2: Gary is green.[(((((triple8) -> rule1)) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
((triple6) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
((triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple7
((triple1 triple6) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Gary is red.
("Gary" "is" "red" "+")
triple10
Gary is rough.
("Gary" "is" "rough" "+")
triple11
Gary is smart.
("Gary" "is" "smart" "+")
triple12
((triple8 ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((triple8) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2