Bob is big. Bob is green. Bob is quiet. Bob is smart. Charlie is nice. Charlie is quiet. Charlie is smart. Harry is nice. Harry is quiet. Harry is young. Smart people are green. If someone is smart then they are big. If someone is smart then they are young. All green people are smart. If Bob is big and Bob is quiet then Bob is green. If Bob is big then Bob is white. If someone is smart then they are nice. All nice people are white.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is young.
("Harry" "is" "young" "+")
Smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If someone is smart then they are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If someone is smart then they are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
All green people are smart.
((("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
If Bob is big and Bob is quiet then Bob is green.
((("Bob" "is" "big" "+") ("Bob" "is" "quiet" "+")) -> ("Bob" "is" "green" "+"))
If Bob is big then Bob is white.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "white" "+"))
If someone is smart then they are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
All nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
Bob is smart.
True
1
proof
[(triple4 OR ((triple2) -> rule4) OR ((((triple1 triple3) -> rule5)) -> rule4))]
("Bob" "is" "smart" "+")
triple4
((triple2) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple1 triple3) -> (rule5 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not green.
False
1
inv-proof
[(triple2 OR ((triple4) -> rule1) OR ((triple1 triple3) -> rule5) OR ((((triple4) -> rule2) triple3) -> rule5))]
("Bob" "is" "green" "-")
triple2
((triple4) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple1 triple3) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple4) -> (rule2 % int2)) triple3) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
@0: Bob is big.[(triple1 OR ((triple4) -> rule2) OR ((((triple2) -> rule4)) -> rule2))] Bob is green.[(triple2 OR ((triple4) -> rule1) OR ((triple1 triple3) -> rule5) OR ((((triple4) -> rule2) triple3) -> rule5))] Bob is quiet.[(triple3)] Bob is smart.[(triple4 OR ((triple2) -> rule4) OR ((((triple1 triple3) -> rule5)) -> rule4))] Charlie is nice.[(triple5 OR ((triple7) -> rule7))] Charlie is quiet.[(triple6)] Charlie is smart.[(triple7)] Harry is nice.[(triple8)] Harry is quiet.[(triple9)] Harry is young.[(triple10)] @1: Bob is nice.[(((triple4) -> rule7) OR ((((triple2) -> rule4)) -> rule7) OR ((((((triple1 triple3) -> rule5)) -> rule4)) -> rule7))] Bob is white.[(((triple1) -> rule6) OR ((((triple4) -> rule2)) -> rule6) OR ((((triple4) -> rule7)) -> rule8) OR ((((((triple2) -> rule4)) -> rule2)) -> rule6) OR ((((((triple2) -> rule4)) -> rule7)) -> rule8) OR ((((((((triple1 triple3) -> rule5)) -> rule4)) -> rule7)) -> rule8))] Bob is young.[(((triple4) -> rule3) OR ((((triple2) -> rule4)) -> rule3) OR ((((((triple1 triple3) -> rule5)) -> rule4)) -> rule3))] Charlie is big.[(((triple7) -> rule2))] Charlie is green.[(((triple7) -> rule1))] Charlie is white.[(((triple5) -> rule8) OR ((((triple7) -> rule7)) -> rule8))] Charlie is young.[(((triple7) -> rule3))] Harry is white.[(((triple8) -> rule8))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple4) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple2
((triple4) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple1 triple3) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple4) -> (rule2 % int2)) triple3) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
((triple2) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple1 triple3) -> (rule5 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
((triple7) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple8
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Bob is nice.
("Bob" "is" "nice" "+")
((triple4) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((((triple1 triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple4) -> (rule7 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((((triple1 triple3) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is young.
("Bob" "is" "young" "+")
((triple4) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((((triple1 triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
((triple7) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple7) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple5) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple7) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((triple7) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple8) -> (rule8 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1