Bob is big. Bob is nice. Bob is quiet. Bob is red. Bob is rough. Bob is round. Dave is big. Dave is cold. Dave is nice. Dave is quiet. Dave is rough. Dave is round. All big, nice people are rough. All big people are rough. Quiet people are cold.
Bob is big.
("Bob" "is" "big" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
All big, nice people are rough.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
All big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Quiet people are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
Dave is cold.
True
1
proof
[(triple8 OR ((triple10) -> rule3))]
("Dave" "is" "cold" "+")
triple8
((triple10) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not rough.
False
1
inv-proof
[(triple11 OR ((triple7) -> rule2) OR ((triple7 triple9) -> rule1))]
("Dave" "is" "rough" "-")
triple11
((triple7) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple7 triple9) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Bob is cold.
True
2
proof
[(((triple3) -> rule3))]
("Bob" "is" "cold" "+")
((triple3) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple3) -> rule3))]
("Bob" "is" "cold" "-")
((triple3) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
@0: Bob is big.[(triple1)] Bob is nice.[(triple2)] Bob is quiet.[(triple3)] Bob is red.[(triple4)] Bob is rough.[(triple5 OR ((triple1) -> rule2) OR ((triple1 triple2) -> rule1))] Bob is round.[(triple6)] Dave is big.[(triple7)] Dave is cold.[(triple8 OR ((triple10) -> rule3))] Dave is nice.[(triple9)] Dave is quiet.[(triple10)] Dave is rough.[(triple11 OR ((triple7) -> rule2) OR ((triple7 triple9) -> rule1))] Dave is round.[(triple12)] @1: Bob is cold.[(((triple3) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple1) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple1 triple2) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple6
Dave is big.
("Dave" "is" "big" "+")
triple7
Dave is cold.
("Dave" "is" "cold" "+")
triple8
((triple10) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple9
Dave is quiet.
("Dave" "is" "quiet" "+")
triple10
Dave is rough.
("Dave" "is" "rough" "+")
triple11
((triple7) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple7 triple9) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple12
Bob is cold.
("Bob" "is" "cold" "+")
((triple3) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1