Charlie is blue. Charlie is kind. Charlie is smart. Dave is big. Dave is blue. Dave is cold. Dave is kind. Dave is quiet. Dave is smart. Dave is white. If someone is kind then they are quiet. If someone is smart then they are big. If someone is kind and quiet then they are white.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
If someone is kind then they are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If someone is smart then they are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If someone is kind and quiet then they are white.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Dave is white.
True
1
proof
[(triple10 OR ((triple7 triple8) -> rule3) OR ((triple7 ((triple7) -> rule1)) -> rule3))]
("Dave" "is" "white" "+")
triple10
((triple7 triple8) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple7 ((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not blue.
False
1
inv-proof
[(triple5)]
("Dave" "is" "blue" "-")
triple5
Charlie is big.
True
2
proof
[(((triple3) -> rule2))]
("Charlie" "is" "big" "+")
((triple3) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple2) -> rule1))]
("Charlie" "is" "quiet" "-")
((triple2) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
True
4
proof
[(((triple2 ((triple2) -> rule1)) -> rule3))]
("Charlie" "is" "white" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not white.
False
4
inv-proof
[(((triple2 ((triple2) -> rule1)) -> rule3))]
("Charlie" "is" "white" "-")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
@0: Charlie is blue.[(triple1)] Charlie is kind.[(triple2)] Charlie is smart.[(triple3)] Dave is big.[(triple4 OR ((triple9) -> rule2))] Dave is blue.[(triple5)] Dave is cold.[(triple6)] Dave is kind.[(triple7)] Dave is quiet.[(triple8 OR ((triple7) -> rule1))] Dave is smart.[(triple9)] Dave is white.[(triple10 OR ((triple7 triple8) -> rule3) OR ((triple7 ((triple7) -> rule1)) -> rule3))] @1: Charlie is big.[(((triple3) -> rule2))] Charlie is quiet.[(((triple2) -> rule1))] @2: Charlie is white.[(((triple2 ((triple2) -> rule1)) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
((triple9) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is cold.
("Dave" "is" "cold" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
((triple7) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple9
Dave is white.
("Dave" "is" "white" "+")
triple10
((triple7 triple8) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple7 ((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((triple3) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2