Bob is big. Bob is blue. Bob is quiet. Bob is rough. Bob is round. Bob is smart. Bob is young. Dave is big. Dave is round. Dave is smart. Dave is young. Erin is big. Erin is quiet. Erin is round. Erin is smart. Erin is young. All quiet things are rough. Round, quiet things are blue. If Erin is young then Erin is round. If something is round then it is rough. If something is round then it is big. If something is smart then it is blue. All rough things are big. If something is young and smart then it is rough.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
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 round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
All quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Round, quiet things are blue.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If Erin is young then Erin is round.
((("Erin" "is" "young" "+")) -> ("Erin" "is" "round" "+"))
If something is round then it is rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If something is round then it is big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If something is smart then it is blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
All rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is young and smart then it is rough.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
Bob is quiet.
True
1
proof
[(triple3)]
("Bob" "is" "quiet" "+")
triple3
Bob is not rough.
False
1
inv-proof
[(triple4 OR ((triple3) -> rule1) OR ((triple5) -> rule4) OR ((triple7 triple6) -> rule8))]
("Bob" "is" "rough" "-")
triple4
((triple3) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple5) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple7 triple6) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
@0: Bob is big.[(triple1 OR ((triple4) -> rule7) OR ((triple5) -> rule5) OR ((((triple3) -> rule1)) -> rule7) OR ((((triple5) -> rule4)) -> rule7) OR ((((triple7 triple6) -> rule8)) -> rule7))] Bob is blue.[(triple2 OR ((triple6) -> rule6) OR ((triple5 triple3) -> rule2))] Bob is quiet.[(triple3)] Bob is rough.[(triple4 OR ((triple3) -> rule1) OR ((triple5) -> rule4) OR ((triple7 triple6) -> rule8))] Bob is round.[(triple5)] Bob is smart.[(triple6)] Bob is young.[(triple7)] Dave is big.[(triple8 OR ((triple9) -> rule5) OR ((((triple9) -> rule4)) -> rule7) OR ((((triple11 triple10) -> rule8)) -> rule7))] Dave is round.[(triple9)] Dave is smart.[(triple10)] Dave is young.[(triple11)] Erin is big.[(triple12 OR ((triple14) -> rule5) OR ((((triple13) -> rule1)) -> rule7) OR ((((triple14) -> rule4)) -> rule7) OR ((((triple16) -> rule3)) -> rule5) OR ((((triple16 triple15) -> rule8)) -> rule7) OR ((((((triple16) -> rule3)) -> rule4)) -> rule7))] Erin is quiet.[(triple13)] Erin is round.[(triple14 OR ((triple16) -> rule3))] Erin is smart.[(triple15)] Erin is young.[(triple16)] @1: Dave is blue.[(((triple10) -> rule6))] Dave is rough.[(((triple9) -> rule4) OR ((triple11 triple10) -> rule8))] Erin is blue.[(((triple15) -> rule6) OR ((triple14 triple13) -> rule2) OR ((((triple16) -> rule3) triple13) -> rule2))] Erin is rough.[(((triple13) -> rule1) OR ((triple14) -> rule4) OR ((triple16 triple15) -> rule8) OR ((((triple16) -> rule3)) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple4) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple5) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple5) -> (rule4 % int2))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple7 triple6) -> (rule8 % int2))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple6) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple5 triple3) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
((triple3) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple5) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple7 triple6) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
((triple9) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple9) -> (rule4 % int2))) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple11 triple10) -> (rule8 % int2))) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
triple9
Dave is smart.
("Dave" "is" "smart" "+")
triple10
Dave is young.
("Dave" "is" "young" "+")
triple11
Erin is big.
("Erin" "is" "big" "+")
triple12
((triple14) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple13) -> (rule1 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple14) -> (rule4 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple16) -> (rule3 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple16 triple15) -> (rule8 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((((triple16) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple13
Erin is round.
("Erin" "is" "round" "+")
triple14
((triple16) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple15
Erin is young.
("Erin" "is" "young" "+")
triple16
Dave is blue.
("Dave" "is" "blue" "+")
((triple10) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple9) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple11 triple10) -> (rule8 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple15) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple14 triple13) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple16) -> (rule3 % int2)) triple13) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((triple13) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple14) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple16 triple15) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple16) -> (rule3 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2