Bob is big. Bob is cold. Bob is green. Bob is red. Bob is smart. Dave is big. Dave is blue. Dave is not cold. Dave is green. Dave is quiet. Dave is red. Dave is smart. Cold things are quiet. Green things are quiet. If something is big and cold then it is red. All green things are red. All green things are big. If something is quiet and red then it is green. If something is red and cold then it is smart. If something is smart and not quiet then it is blue.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
Green things are quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is big and cold then it is red.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
All green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is quiet and red then it is green.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something is red and cold then it is smart.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If something is smart and not quiet then it is blue.
((("something" "is" "smart" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "blue" "+"))
Dave is quiet.
True
1
proof
[(triple10 OR ((triple9) -> rule2))]
("Dave" "is" "quiet" "+")
triple10
((triple9) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Bob is not big.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule5) OR ((((((triple2) -> rule1) triple4) -> rule6)) -> rule5))]
("Bob" "is" "big" "-")
triple1
((triple3) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((((triple2) -> (rule1 % int3)) triple4) -> (rule6 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is quiet.
True
2
proof
[(((triple2) -> rule1) OR ((triple3) -> rule2))]
("Bob" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple3) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple2) -> rule1) OR ((triple3) -> rule2))]
("Bob" "is" "quiet" "-")
((triple2) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple3) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
@0: Bob is big.[(triple1 OR ((triple3) -> rule5) OR ((((((triple2) -> rule1) triple4) -> rule6)) -> rule5))] Bob is cold.[(triple2)] Bob is green.[(triple3 OR ((((triple2) -> rule1) triple4) -> rule6) OR ((((triple2) -> rule1) ((triple1 triple2) -> rule3)) -> rule6))] Bob is red.[(triple4 OR ((triple3) -> rule4) OR ((triple1 triple2) -> rule3) OR ((((triple3) -> rule5) triple2) -> rule3))] Bob is smart.[(triple5 OR ((triple4 triple2) -> rule7) OR ((((triple3) -> rule4) triple2) -> rule7) OR ((((triple1 triple2) -> rule3) triple2) -> rule7) OR ((((((triple3) -> rule5) triple2) -> rule3) triple2) -> rule7))] Dave is big.[(triple6 OR ((triple9) -> rule5) OR ((((triple10 triple11) -> rule6)) -> rule5))] Dave is blue.[(triple7)] Dave is green.[(triple9 OR ((triple10 triple11) -> rule6))] Dave is not cold.[(triple8)] Dave is quiet.[(triple10 OR ((triple9) -> rule2))] Dave is red.[(triple11 OR ((triple9) -> rule4))] Dave is smart.[(triple12)] @1: Bob is quiet.[(((triple2) -> rule1) OR ((triple3) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple3) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((((triple2) -> (rule1 % int3)) triple4) -> (rule6 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
((((triple2) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple2) -> (rule1 % int3)) ((triple1 triple2) -> (rule3 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple3) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple1 triple2) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple3) -> (rule5 % int2)) triple2) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
triple5
((triple4 triple2) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple3) -> (rule4 % int2)) triple2) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple1 triple2) -> (rule3 % int2)) triple2) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((((triple3) -> (rule5 % int3)) triple2) -> (rule3 % int2)) triple2) -> (rule7 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
triple6
((triple9) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple10 triple11) -> (rule6 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
triple7
Dave is green.
("Dave" "is" "green" "+")
triple9
((triple10 triple11) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not cold.
("Dave" "is" "cold" "-")
triple8
Dave is quiet.
("Dave" "is" "quiet" "+")
triple10
((triple9) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple11
((triple9) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple12
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple3) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1