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