Bob is blue. Bob is cold. Bob is kind. Bob is quiet. Bob is round. Bob is smart. Bob is young. Dave is blue. Dave is cold. Dave is round. All young things are quiet. All quiet things are smart. Round, blue things are young.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is round.
("Dave" "is" "round" "+")
All young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
All quiet things are smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Round, blue things are young.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Dave is cold.
True
1
proof
[(triple9)]
("Dave" "is" "cold" "+")
triple9
Bob is not quiet.
False
1
inv-proof
[(triple4 OR ((triple7) -> rule1) OR ((((triple5 triple1) -> rule3)) -> rule1))]
("Bob" "is" "quiet" "-")
triple4
((triple7) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple5 triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Dave is young.
True
3
proof
[(((triple10 triple8) -> rule3))]
("Dave" "is" "young" "+")
((triple10 triple8) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
3
inv-proof
[(((triple10 triple8) -> rule3))]
("Dave" "is" "young" "-")
((triple10 triple8) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is quiet.
True
4
proof
[(((((triple10 triple8) -> rule3)) -> rule1))]
("Dave" "is" "quiet" "+")
((((triple10 triple8) -> (rule3 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not quiet.
False
4
inv-proof
[(((((triple10 triple8) -> rule3)) -> rule1))]
("Dave" "is" "quiet" "-")
((((triple10 triple8) -> (rule3 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is smart.
True
5
proof
[(((((((triple10 triple8) -> rule3)) -> rule1)) -> rule2))]
("Dave" "is" "smart" "+")
((((((triple10 triple8) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not smart.
False
5
inv-proof
[(((((((triple10 triple8) -> rule3)) -> rule1)) -> rule2))]
("Dave" "is" "smart" "-")
((((((triple10 triple8) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2)] Bob is kind.[(triple3)] Bob is quiet.[(triple4 OR ((triple7) -> rule1) OR ((((triple5 triple1) -> rule3)) -> rule1))] Bob is round.[(triple5)] Bob is smart.[(triple6 OR ((triple4) -> rule2) OR ((((triple7) -> rule1)) -> rule2) OR ((((((triple5 triple1) -> rule3)) -> rule1)) -> rule2))] Bob is young.[(triple7 OR ((triple5 triple1) -> rule3))] Dave is blue.[(triple8)] Dave is cold.[(triple9)] Dave is round.[(triple10)] @1: Dave is young.[(((triple10 triple8) -> rule3))] @2: Dave is quiet.[(((((triple10 triple8) -> rule3)) -> rule1))] @3: Dave is smart.[(((((((triple10 triple8) -> rule3)) -> rule1)) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple7) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple5 triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple4) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple5 triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple5 triple1) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple8
Dave is cold.
("Dave" "is" "cold" "+")
triple9
Dave is round.
("Dave" "is" "round" "+")
triple10
Dave is young.
("Dave" "is" "young" "+")
((triple10 triple8) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple10 triple8) -> (rule3 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((((triple10 triple8) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3