Bob is white. Dave is white. Smart things are not round. All white things are big. All kind things are quiet. If something is big then it is quiet. If something is quiet and smart then it is cold. All big things are smart. If something is cold and big then it is kind. Big things are white.
Bob is white.
("Bob" "is" "white" "+")
Dave is white.
("Dave" "is" "white" "+")
Smart things are not round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "-"))
All white things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
All kind things are quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If something is big then it is quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet and smart then it is cold.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
All big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If something is cold and big then it is kind.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
Dave is white.
True
1
proof
[(triple2)]
("Dave" "is" "white" "+")
triple2
Dave is not white.
False
1
inv-proof
[(triple2)]
("Dave" "is" "white" "-")
triple2
Bob is big.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "big" "+")
((triple1) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "big" "-")
((triple1) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Dave is smart.
True
3
proof
[(((((triple2) -> rule2)) -> rule6))]
("Dave" "is" "smart" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Bob is not smart.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule6))]
("Bob" "is" "smart" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is cold.
True
7
proof
[(((((((triple1) -> rule2)) -> rule4) ((((triple1) -> rule2)) -> rule6)) -> rule5))]
("Bob" "is" "cold" "+")
((((((triple1) -> (rule2 % int4))) -> (rule4 % int3)) ((((triple1) -> (rule2 % int4))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is not cold.
False
7
inv-proof
[(((((((triple1) -> rule2)) -> rule4) ((((triple1) -> rule2)) -> rule6)) -> rule5))]
("Bob" "is" "cold" "-")
((((((triple1) -> (rule2 % int4))) -> (rule4 % int3)) ((((triple1) -> (rule2 % int4))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
@0: Bob is white.[(triple1)] Dave is white.[(triple2)] @1: Bob is big.[(((triple1) -> rule2))] Dave is big.[(((triple2) -> rule2))] @2: Bob is quiet.[(((((triple1) -> rule2)) -> rule4))] Bob is smart.[(((((triple1) -> rule2)) -> rule6))] Dave is quiet.[(((((triple2) -> rule2)) -> rule4))] Dave is smart.[(((((triple2) -> rule2)) -> rule6))] @3: Bob is cold.[(((((((triple1) -> rule2)) -> rule4) ((((triple1) -> rule2)) -> rule6)) -> rule5))] Bob is not round.[(((((((triple1) -> rule2)) -> rule6)) -> rule1))] Dave is cold.[(((((((triple2) -> rule2)) -> rule4) ((((triple2) -> rule2)) -> rule6)) -> rule5))] Dave is not round.[(((((((triple2) -> rule2)) -> rule6)) -> rule1))] @4: Bob is kind.[(((((((((triple1) -> rule2)) -> rule4) ((((triple1) -> rule2)) -> rule6)) -> rule5) ((triple1) -> rule2)) -> rule7))] Dave is kind.[(((((((((triple2) -> rule2)) -> rule4) ((((triple2) -> rule2)) -> rule6)) -> rule5) ((triple2) -> rule2)) -> rule7))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((((triple1) -> (rule2 % int4))) -> (rule4 % int3)) ((((triple1) -> (rule2 % int4))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is not round.
("Bob" "is" "round" "-")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Bob is not round.
("Bob" "is" "round" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
((((((triple2) -> (rule2 % int4))) -> (rule4 % int3)) ((((triple2) -> (rule2 % int4))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is not round.
("Dave" "is" "round" "-")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
((((((((triple1) -> (rule2 % int5))) -> (rule4 % int4)) ((((triple1) -> (rule2 % int5))) -> (rule6 % int3))) -> (rule5 % int2)) ((triple1) -> (rule2 % int5))) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is big.
("Bob" "is" "big" "+")
int5
Dave is kind.
("Dave" "is" "kind" "+")
((((((((triple2) -> (rule2 % int5))) -> (rule4 % int4)) ((((triple2) -> (rule2 % int5))) -> (rule6 % int3))) -> (rule5 % int2)) ((triple2) -> (rule2 % int5))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is big.
("Dave" "is" "big" "+")
int5